feat: use getEqnsFor? at simp

src/Lean/Meta/Tactic/Simp/SimpLemmas.lean

@@ -7,6 +7,7 @@ import Lean.ScopedEnvExtension
 import Lean.Util.Recognizers
 import Lean.Meta.DiscrTree
 import Lean.Meta.AppBuilder
+import Lean.Meta.Eqns
 import Lean.Meta.Tactic.AuxLemma
 namespace Lean.Meta
 
@@ -66,7 +67,7 @@ where
     | none => s
     | some name => s.insert name
 
-def SimpLemmas.addDeclToUnfold (d : SimpLemmas) (declName : Name) : SimpLemmas :=
+def SimpLemmas.addDeclToUnfoldCore (d : SimpLemmas) (declName : Name) : SimpLemmas :=
   { d with toUnfold := d.toUnfold.insert declName }
 
 def SimpLemmas.isDeclToUnfold (d : SimpLemmas) (declName : Name) : Bool :=
@@ -220,7 +221,7 @@ def mkSimpExt (extName : Name) : IO SimpExtension :=
     addEntry := fun d e =>
       match e with
       | SimpEntry.lemma e => addSimpLemmaEntry d e
-      | SimpEntry.toUnfold n => d.addDeclToUnfold n
+      | SimpEntry.toUnfold n => d.addDeclToUnfoldCore n
   }
 
 def registerSimpAttr (attrName : Name) (attrDescr : String) (extName : Name := attrName.appendAfter "Ext") : IO SimpExtension := do
@@ -281,4 +282,16 @@ where
       else
         return none
 
+def SimpLemmas.addDeclToUnfold (d : SimpLemmas) (declName : Name) : MetaM SimpLemmas := do
+  if hasSmartUnfoldingDecl (← getEnv) declName then
+    return d.addDeclToUnfoldCore declName
+  else withLCtx {} {} do
+    if let some eqns ← getEqnsFor? declName then
+      let mut d := d
+      for eqn in eqns do
+        d ← SimpLemmas.addConst d eqn
+      return d
+    else
+      return d.addDeclToUnfoldCore declName
+
 end Lean.Meta

src/Lean/Meta/WHNF.lean

@@ -23,6 +23,9 @@ def smartUnfoldingSuffix := "_sunfold"
 @[inline] def mkSmartUnfoldingNameFor (declName : Name) : Name :=
   Name.mkStr declName smartUnfoldingSuffix
 
+def hasSmartUnfoldingDecl (env : Environment) (declName : Name) : Bool :=
+  env.contains (mkSmartUnfoldingNameFor declName)
+
 register_builtin_option smartUnfolding : Bool := {
   defValue := true
   descr := "when computing weak head normal form, use auxiliary definition created for functions defined by structural recursion"

tests/lean/run/eqnsAtSimp.lean

@@ -0,0 +1,19 @@
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by measure fun
+  | Sum.inl n => n
+  | Sum.inr n => n
+decreasing_by
+  simp [measure, invImage, InvImage, Nat.lt_wfRel]
+  apply Nat.lt_succ_self
+
+theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
+  induction x with
+  | zero => simp
+  | succ x ih => simp [Nat.mul_succ, Nat.add_succ, isEven, isOdd, ih]