From b4a1ca15a28e78ac8a9035505103c272195413a9 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 7 Nov 2024 17:05:21 +0100 Subject: [PATCH] `getUnfoldableConst*?` should only return defs/theorems --- src/Lean/Meta/ExprDefEq.lean | 5 +---- src/Lean/Meta/GetUnfoldableConst.lean | 7 +++---- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 41f47d18eaf9..6314ee8f08f3 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/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 -/ diff --git a/src/Lean/Meta/GetUnfoldableConst.lean b/src/Lean/Meta/GetUnfoldableConst.lean index 634b25de03ec..1a5fdde385e5 100644 --- a/src/Lean/Meta/GetUnfoldableConst.lean +++ b/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