diff options
| author | Jim Fehrle | 2021-03-07 10:15:11 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-03-30 09:51:56 -0700 |
| commit | eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf (patch) | |
| tree | 6057d6c11961f6398fcca77313b0e8abcaaa8961 /doc/sphinx/language | |
| parent | 16d9e9cf378b9eb0ee0fc42c5c0a3a23b3df6ff4 (diff) | |
Remove the :> type cast
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index fcf61a5bf4..1a729ced4e 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -42,7 +42,6 @@ Type cast term_cast ::= @term10 : @type | @term10 <: @type | @term10 <<: @type - | @term10 :> The expression :n:`@term10 : @type` is a type cast expression. It enforces the type of :n:`@term10` to be :n:`@type`. @@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`). :n:`@term10 <<: @type` specifies that compilation to OCaml will be used to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`). -:n:`@term10 :>` casts to the support type in Program mode. -See :ref:`syntactic_control`. - .. _gallina-definitions: Top-level definitions |