diff options
Diffstat (limited to 'doc/sphinx/language/extensions')
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index d6a828521f..34752a4c4d 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -90,6 +90,10 @@ 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 |