max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: mention the proof-binding syntax in match

Browse source 
This comes up over and over again in the zulip; let's document it!
This commit is contained in:
Eric Wieser 2023-11-06 11:57:10 +00:00 • committed by Leonardo de Moura
parent 995725b256
commit 72f7144403
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Parser/Term.lean
View file

@ -351,6 +351,9 @@ term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.