diff options
| author | Théo Zimmermann | 2020-05-14 10:47:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 10:47:18 +0200 |
| commit | 1e04e6de348160cf40292184cfafed459a9219d7 (patch) | |
| tree | f7ee9e86e2938db50f28d04b0d0b52681ee86fe9 | |
| parent | fb9719d915a19853ce06274e4f27aaaad50a970c (diff) | |
| parent | 0867c1d11264b39d00f117da29cbb9d1fa1f911d (diff) | |
Merge definitions and type casts in same file.
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index ea3be3fd4e..679022a5b1 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -1,3 +1,6 @@ +Definitions +=========== + .. index:: let ... := ... (term) .. _let-in: @@ -20,6 +23,31 @@ denotes the local binding of :n:`@term` to the variable definition of functions: :n:`let @ident {+ @binder} := @term in @term’` stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. +.. index:: + single: ... : ... (type cast) + single: ... <: ... + single: ... <<: ... + +Type cast +--------- + +.. insertprodn term_cast term_cast + +.. prodn:: + term_cast ::= @term10 <: @term + | @term10 <<: @term + | @term10 : @term + | @term10 :> + +The expression :n:`@term : @type` is a type cast expression. It enforces +the type of :n:`@term` to be :n:`@type`. + +:n:`@term <: @type` locally sets up the virtual machine for checking that +:n:`@term` has type :n:`@type`. + +:n:`@term <<: @type` uses native compilation for checking that :n:`@term` +has type :n:`@type`. + .. _gallina-definitions: Top-level definitions |