From c17a1c382f85c04fad7cd23cabaff6b2a0c214e5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Feb 2021 09:19:37 -0800
Subject: [PATCH] fix: `isDeltaCandidate?`

It should return `some ...` only if `ConstantInfo` has a value.
---
 src/Lean/Meta/ExprDefEq.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index adf6740397..c87047485b 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -938,10 +938,13 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
     else
       return false
 
-private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) :=
+private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do
   match t.getAppFn with
-  | Expr.const c _ _ => getConst? c
-  | _                => pure none
+  | Expr.const c _ _ =>
+    match (← getConst? c) with
+    | r@(some info) => if info.hasValue then return r else return none
+    | _             => return none
+  | _ => pure none
 
 /-- Auxiliary method for isDefEqDelta -/
 private def isListLevelDefEq (us vs : List Level) : MetaM LBool :=