aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/extensions/match.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language/extensions/match.rst')
-rw-r--r--doc/sphinx/language/extensions/match.rst7
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 23389eba3b..8e62c2af13 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -86,6 +86,13 @@ Pattern-matching on terms inhabiting inductive type having only one
constructor can be alternatively written using :g:`let … in …`
constructions. There are two variants of them.
+.. insertprodn destructuring_let destructuring_let
+
+.. prodn::
+ destructuring_let ::= let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
+ | let ' @pattern := @term {? return @term100 } in @term
+ | let ' @pattern in @pattern := @term return @term100 in @term
+
First destructuring let syntax
++++++++++++++++++++++++++++++