From 69be2148d6a2c403d75185ea205f263207692a64 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jan 2020 16:29:59 -0800 Subject: [PATCH] chore: remove buggy optimization --- src/Init/Lean/Meta/ExprDefEq.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean index 877b035cb4..3f98f6d5f5 100644 --- a/src/Init/Lean/Meta/ExprDefEq.lean +++ b/src/Init/Lean/Meta/ExprDefEq.lean @@ -945,6 +945,8 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool condM (isSynthetic sFn <&&> synthPending sFn) (do s ← instantiateMVars s; isDefEqQuick t s) $ do tAssign? ← isAssignable tFn; sAssign? ← isAssignable sFn; + trace! `Meta.isDefEq + (t ++ (if tAssign? then " [assignable]" else " [nonassignable]") ++ " =?= " ++ s ++ (if sAssign? then " [assignable]" else " [nonassignable]")); let assign (t s : Expr) : MetaM LBool := toLBoolM $ processAssignment t s; cond (tAssign? && !sAssign?) (assign t s) $ cond (!tAssign? && sAssign?) (assign s t) $ @@ -959,8 +961,6 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool -- Both `t` and `s` are terms of the form `?m ...` tMVarDecl ← getMVarDecl tFn.mvarId!; sMVarDecl ← getMVarDecl sFn.mvarId!; - cond (!sMVarDecl.lctx.isSubPrefixOf tMVarDecl.lctx) (assign s t) $ - cond (!tMVarDecl.lctx.isSubPrefixOf sMVarDecl.lctx) (assign t s) $ if s.isMVar && !t.isMVar then /- Solve `?m t =?= ?n` by trying first `?n := ?m t`. Reason: this assignment is precise. -/