diff options
Diffstat (limited to 'doc/sphinx/language/extensions/match.rst')
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 7 |
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 ++++++++++++++++++++++++++++++ |
