diff options
Diffstat (limited to 'doc/sphinx/language/extensions')
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index b4558ef07f..34752a4c4d 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -90,11 +90,15 @@ constructions. There are two variants of them. First destructuring let syntax ++++++++++++++++++++++++++++++ +.. todo explain that this applies to all of the "let" constructs (Gallina, Ltac1 and Ltac2) + also add "irrefutable pattern" to the glossary + note that in Ltac2 an upper case ident is a constructor, lower case is a variable + The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1` performs case analysis on :n:`@term__0` whose type must be an inductive type with exactly one constructor. The number of variables :n:`@ident__i` must correspond to the number of arguments of this -contrustor. Then, in :n:`@term__1`, these variables are bound to the +constructor. Then, in :n:`@term__1`, these variables are bound to the arguments of the constructor in :n:`@term__0`. For instance, the definition |