Move destructuring let syntax closer to its documentation.

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
 ++++++++++++++++++++++++++++++