From 15183aafe292695c54ae234a1210c08c8e3cd378 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 13 Nov 2020 10:08:48 +0100
Subject: Move destructuring let syntax closer to its documentation.

---
 doc/sphinx/language/core/definitions.rst | 21 ++++++++++++---------
 doc/sphinx/language/extensions/match.rst |  7 +++++++
 2 files changed, 19 insertions(+), 9 deletions(-)

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 4ea3ea5e6d..79489c85f6 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -13,15 +13,18 @@ Let-in definitions
 .. prodn::
    term_let ::= let @name {? : @type } := @term in @term
    | let @name {+ @binder } {? : @type } := @term in @term
-   | 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
-
-:n:`let @ident := @term in @term’`
-denotes the local binding of :n:`@term` to the variable
-:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in
-definition of functions: :n:`let @ident {+ @binder} := @term in @term’`
-stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
+   | @destructuring_let
+
+:n:`let @ident := @term__1 in @term__2` represents the local binding of
+the variable :n:`@ident` to the value :n:`@term__1` in :n:`@term__2`.
+
+:n:`let @ident {+ @binder} := @term__1 in @term__2` is an abbreviation
+for :n:`let @ident := fun {+ @binder} => @term__1 in @term__2`.
+
+.. seealso::
+
+   Extensions of the `let ... in ...` syntax are described in
+   :ref:`irrefutable-patterns`.
 
 .. index::
    single: ... : ... (type cast)
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
 ++++++++++++++++++++++++++++++
-- 
cgit v1.2.3