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

chore: update

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-02 12:12:27 -07:00
parent ba7f2849dc
commit f8c5face56
1 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/elabissues/issues1.lean
View file

@ -5,14 +5,7 @@ f [1, 2, 3] -- Works
def ex2 : Bool :=
let xs := [1, 2, 3];
/- The following application fails.
In the Lean3 elaborator, the `;` after `have` and `let` expressions is a "check-point".
The elaborator will resolve type class instances and force pending numeral types to `Nat` if they
have not been assigned yet.
So, `xs` will have type `List Nat`.
Solution: remove "check-point" from `let`, but keep the one on `have`. We use `have` expressions
when proving, and it is nice to make sure the proposition does not have meta-variables before continuing. -/
f xs
f xs -- Works
def ex3 : IO Bool :=
do