aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/orderedGrammar
diff options
context:
space:
mode:
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
-rw-r--r--doc/tools/docgram/orderedGrammar4
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index c697043f27..6b12d90d5d 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -473,6 +473,10 @@ ssr_dpat: [
term_let: [
| "let" name OPT ( ":" type ) ":=" term "in" term
| "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
+| destructuring_let
+]
+
+destructuring_let: [
| "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term
| "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term
| "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term