From 0867c1d11264b39d00f117da29cbb9d1fa1f911d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 14 May 2020 10:42:07 +0200
Subject: Add type casts to new Definitions file.

---
 doc/sphinx/language/core/definitions.rst | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 doc/sphinx/language/core/definitions.rst

(limited to 'doc/sphinx/language/core')

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`.
-- 
cgit v1.2.3