From 856fb0c0005d77895883eed2dc47766991ce9e42 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Nov 2019 08:41:26 -0800
Subject: [PATCH] feat: use `isProofQuick` to implement `isDefEqProofIrrel`

---
 src/Init/Lean/Meta/ExprDefEq.lean | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index 3b61289b90..306cb77bb2 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -940,10 +940,19 @@ private partial def isDefEqQuick : Expr → Expr → MetaM LBool
   assign t s
 
 private def isDefEqProofIrrel (t s : Expr) : MetaM LBool :=
-do tType ← inferType t;
-   condM (isProp tType)
-     (do sType ← inferType s; toLBoolM $ isExprDefEqAux tType sType)
-     (pure LBool.undef)
+do status ← isProofQuick t;
+   match status with
+   | LBool.false =>
+     pure LBool.undef
+   | LBool.true  => do
+     tType ← inferType t;
+     sType ← inferType s;
+     toLBoolM $ isExprDefEqAux tType sType
+   | LBool.undef => do
+     tType ← inferType t;
+     condM (isProp tType)
+       (do sType ← inferType s; toLBoolM $ isExprDefEqAux tType sType)
+       (pure LBool.undef)
 
 @[inline] def tryL (x : MetaM LBool) (k : MetaM Bool) : MetaM Bool :=
 do status ← x;