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

chore: typo

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-02 09:27:31 -08:00
parent d96393ee47
commit 3a08dd2771
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Match.lean
View file

@ -747,7 +747,7 @@ private def elabMatchAux (discrStxs : Array Syntax) (altViews : Array MatchAltVi
| _ => pure ()
```
If `synthesizeSyntheticMVarsNoPostponing`, the example above fails at `x.fst` because
the type of `x` is only available adfer we proces the last argument of `List.forM`.
the type of `x` is only available after we proces the last argument of `List.forM`.
We apply pending default types to make sure we can process examples such as
```