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

fix: eta expansion before lazy delta

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-05 08:33:54 -08:00
parent c7e85e3cec
commit 9626ceda09
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

@ -992,9 +992,9 @@ partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
whenUndefDo (isDefEqQuick t s) $
whenUndefDo (isDefEqProofIrrel t s) $
isDefEqWHNF t s $ fun t s => do
condM (isDefEqEta t s <||> isDefEqEta s t) (pure true) $
whenUndefDo (isDefEqOffset t s) $ do
whenUndefDo (isDefEqDelta t s) $
condM (isDefEqEta t s <||> isDefEqEta s t) (pure true) $
match t, s with
| Expr.const c us _, Expr.const d vs _ => if c == d then isListLevelDefEqAux us vs else pure false
| Expr.app _ _ _, Expr.app _ _ _ =>