refactor: generate equational theorems uniformly

This PR follows upon #10606 and creates equational theorems uniformly
from the unfold theorem, removing the `registerGetEqnsFn` hook.

Author: nomeata

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -403,9 +403,6 @@ Generate equations for `declName`.
 This unfolds the function application on the LHS (using an unfold theorem, if present, or else by
 delta-reduction), calculates the types for the equational theorems using `mkEqnTypes`, and then
 proves them using `mkEqnProof`.
-
-This is currently used for non-recursive functions, well-founded recursion and partial_fixpoint,
-but not for structural recursion.
 -/
 public def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (Array Name) := do
   trace[Elab.definition.eqns] "mkEqns: {.ofConstName declName}"

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

@@ -42,7 +42,10 @@ where
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if (← isRecursiveDefinition declName) then
-    return none
+    let some (.defnInfo info) := (← getEnv).find? declName |
+      throwError "internal error: recursive definition `{declName}` is not a definition"
+    let n ← mkEqns declName info.all.toArray
+    return some n
   if (← getEnv).contains declName then
     if backward.eqns.nonrecursive.get (← getOptions) then
       mkEqns declName #[]

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

@@ -118,14 +118,7 @@ def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   let some info := eqnInfoExt.find? env declName | return none
   return some (← mkUnfoldEq declName info)
 
-def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  if let some info := eqnInfoExt.find? (← getEnv) declName then
-    mkEqns declName info.declNames (tryRefl := false)
-  else
-    return none
-
 builtin_initialize
-  registerGetEqnsFn getEqnsFor?
   registerGetUnfoldEqnFn getUnfoldFor?
 
 end Lean.Elab.PartialFixpoint

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

@@ -151,12 +151,6 @@ public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (r
   modifyEnv fun env => eqnInfoExt.insert env preDef.declName
     { preDef with recArgPos, declNames, fixedParamPerms }
 
-def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  if let some info := eqnInfoExt.find? (← getEnv) declName then
-    mkEqns declName info.declNames
-  else
-    return none
-
 /-- Generate the "unfold" lemma for `declName`. -/
 def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
   let name := mkEqLikeNameFor (← getEnv) info.declName unfoldThmSuffix
@@ -190,7 +184,6 @@ def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
 
 
 builtin_initialize
-  registerGetEqnsFn getEqnsFor?
   registerGetUnfoldEqnFn getUnfoldFor?
   registerTraceClass `Elab.definition.structural.eqns
 

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

@@ -46,16 +46,6 @@ public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Na
           eqnInfoExt.insert env preDef.declName { preDef with
             declNames, declNameNonRec, argsPacker, fixedParamPerms }
 
-def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
-  if let some info := eqnInfoExt.find? (← getEnv) declName then
-    mkEqns declName info.declNames (tryRefl := false)
-  else
-    return none
-
-builtin_initialize
-  registerGetEqnsFn getEqnsFor?
-
-
 /--
 This is a hack to fix fallout from #8519, where a non-exposed wfrec definition `foo`
 in a module would cause `foo.eq_def` to be defined eagerly and privately,

tests/lean/run/partial_fixpoint.lean

@@ -13,7 +13,7 @@ partial_fixpoint
 
 /--
 info: equations:
-theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1)
+@[defeq] theorem loop.eq_1 : ∀ (x : Nat), loop x = loop (x + 1)
 -/
 #guard_msgs in
 #print equations loop