From 8edaddd70c6dd03343ad38320afdf048980d2ab5 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 3 Feb 2025 12:04:07 +0100
Subject: [PATCH] refactor: post-stage0 clean-up for #6898 (#6920)

---
 src/Lean/Elab/PreDefinition/WF/Eqns.lean   | 15 ---------------
 src/Lean/Elab/PreDefinition/WF/Main.lean   |  2 +-
 src/Lean/Elab/PreDefinition/WF/Unfold.lean |  3 +--
 3 files changed, 2 insertions(+), 18 deletions(-)

diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index d5f15d4d00..5a712cc12c 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/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
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index c8bd40fdb1..eb7ee40498 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/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
diff --git a/src/Lean/Elab/PreDefinition/WF/Unfold.lean b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
index 2343f6bc21..51145eccb9 100644
--- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean
+++ b/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