From 9626ceda09830fccecb5ea9b5ca95ac60f47fed1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Mar 2020 08:33:54 -0800 Subject: [PATCH] fix: eta expansion before lazy delta --- src/Init/Lean/Meta/ExprDefEq.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean index 57f6e1f4a2..0fe89b6edd 100644 --- a/src/Init/Lean/Meta/ExprDefEq.lean +++ b/src/Init/Lean/Meta/ExprDefEq.lean @@ -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 _ _ _ =>