refactor: post-stage0 clean-up for #6898

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -51,19 +51,4 @@ def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
 builtin_initialize
   registerGetEqnsFn getEqnsFor?
 
-
--- Remove the rest of this file after the next stage update,
--- as we generate these eagerly now.
-def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
-  let name := Name.str declName unfoldThmSuffix
-  let env ← getEnv
-  if env.contains name then return name
-  let some info := eqnInfoExt.find? env declName | return none
-  mkUnfoldEq info.toEqnInfoCore info.declNameNonRec
-  return some name
-
-builtin_initialize
-  registerGetUnfoldEqnFn getUnfoldFor?
-
-
 end Lean.Elab.WF

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -64,7 +64,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termMeasure?s : Array (Option T
   for preDef in preDefs do
     unless preDef.kind.isTheorem do
       unless (← isProp preDef.type) do
-        WF.mkUnfoldEq { preDef with } preDefNonRec.declName
+        WF.mkUnfoldEq preDef preDefNonRec.declName
   Mutual.addPreDefAttributes preDefs
 
 builtin_initialize registerTraceClass `Elab.definition.wf

src/Lean/Elab/PreDefinition/WF/Unfold.lean

@@ -84,8 +84,7 @@ private partial def mkUnfoldProof (declName declNameNonRec : Name) (type : Expr)
     go mvarId
     instantiateMVars main
 
--- TODO: Afer the next stage0 update, change the type to PreDefinition
-def mkUnfoldEq (preDef : EqnInfoCore) (unaryPreDefName : Name) : MetaM Unit := do
+def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) : MetaM Unit := do
   withOptions (tactic.hygienic.set · false) do
     let baseName := preDef.declName
     lambdaTelescope preDef.value fun xs body => do