Add type casts to new Definitions file.

1 files changed, 24 insertions, 0 deletions

diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
new file mode 100644
index 0000000000..ba48ea130d
--- /dev/null
+++ b/doc/sphinx/language/core/definitions.rst
@@ -0,0 +1,24 @@
+.. 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`.