getUnfoldableConst*? should only return defs/theorems

src/Lean/Meta/ExprDefEq.lean

@@ -1233,10 +1233,7 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
 
 private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do
   match t.getAppFn with
-  | .const c _ =>
-    match (← getUnfoldableConst? c) with
-    | r@(some info) => if info.hasValue then return r else return none
-    | _             => return none
+  | .const c _ => getUnfoldableConst? c
   | _ => pure none
 
 /-- Auxiliary method for isDefEqDelta -/

src/Lean/Meta/GetUnfoldableConst.lean

@@ -30,7 +30,7 @@ def canUnfold (info : ConstantInfo) : MetaM Bool := do
 
 /--
 Look up a constant name, returning the `ConstantInfo`
-if it should be unfolded at the current reducibility settings,
+if it is a def/theorem that should be unfolded at the current reducibility settings,
 or `none` otherwise.
 
 This is part of the implementation of `whnf`.
@@ -40,7 +40,7 @@ def getUnfoldableConst? (constName : Name) : MetaM (Option ConstantInfo) := do
   match (← getEnv).find? constName with
   | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
-  | some info                 => return some info
+  | some _                    => return none
   | none                      => throwUnknownConstant constName
 
 /--
@@ -50,7 +50,6 @@ def getUnfoldableConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) :=
   match (← getEnv).find? constName with
   | some (info@(.thmInfo _))  => getTheoremInfo info
   | some (info@(.defnInfo _)) => if (← canUnfold info) then return info else return none
-  | some info                 => return some info
-  | none                      => return none
+  | _                         => return none
 
 end Meta