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

fix: accidental variable shadowing

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-03 14:38:59 -08:00
parent bae4a5fc7c
commit 1aa398415c
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/Init/Lean/Meta/ExprDefEq.lean
View file

@ -29,7 +29,7 @@ if a.isLambda && !b.isLambda then do
bType ← inferType b;
bType ← whnfUsingDefault bType;
match bType with
| Expr.forallE n d b c =>
| Expr.forallE n d _ c =>
let b' := Lean.mkLambda n c.binderInfo d (mkApp b (mkBVar 0));
try $ isExprDefEqAux a b'
| _ => pure false