feat: save whether a function has been defined by structural or well-founded recursion

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

@@ -101,6 +101,7 @@ def structuralRecursion (preDefs : Array PreDefinition) : TermElabM Unit :=
         -/
         registerEqnsInfo preDef recArgPos
     addSmartUnfoldingDef preDef recArgPos
+    markAsRecursive preDef.declName
     applyAttributesOf #[preDefNonRec] AttributeApplicationTime.afterCompilation
 
 builtin_initialize

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

@@ -144,6 +144,7 @@ def wfRecursion (preDefs : Array PreDefinition) : TermElabM Unit := do
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
   registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
   for preDef in preDefs do
+    markAsRecursive preDef.declName
     applyAttributesOf #[preDef] AttributeApplicationTime.afterCompilation
 
 builtin_initialize registerTraceClass `Elab.definition.wf

src/Lean/Meta/Eqns.lean

@@ -9,6 +9,25 @@ import Lean.Meta.Basic
 import Lean.Meta.AppBuilder
 
 namespace Lean.Meta
+/--
+Environment extension for storing which declarations are recursive.
+This information is populated by the `PreDefinition` module, but the simplifier
+uses when unfolding declarations.
+-/
+builtin_initialize recExt : TagDeclarationExtension ← mkTagDeclarationExtension `recExt
+
+/--
+Marks the given declaration as recursive.
+-/
+def markAsRecursive (declName : Name) : CoreM Unit :=
+  modifyEnv (recExt.tag · declName)
+
+/--
+Returns `true` if `declName` was defined using well-founded recursion, or structural recursion.
+-/
+def isRecursiveDefinition (declName : Name) : CoreM Bool :=
+  return recExt.isTagged (← getEnv) declName
+
 def eqnThmSuffixBase := "eq"
 def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
 def eqn1ThmSuffix := eqnThmSuffixBasePrefix ++ "1"