chore: update stage0

Reason: new builtin environment extension

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"

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

@@ -422,7 +422,20 @@ def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM Si
     let mut d := d
     for eqn in eqns do
       d ← SimpTheorems.addConst d eqn
-    if hasSmartUnfoldingDecl (← getEnv) declName then
+    /-
+    Even if a function has equation theorems,
+    we also store it in the `toUnfold` set in the following two cases:
+    1- It was defined by structural recursion and has a smart-unfolding associated declaration.
+    2- It is non-recursive.
+
+    Reason: `unfoldPartialApp := true` or conditional equations may not apply.
+
+    Remark: In the future, we are planning to disable this
+    behavior unless `unfoldPartialApp := true`.
+    Moreover, users will have to use `f.eq_def` if they want to force the definition to be
+    unfolded.
+    -/
+    if hasSmartUnfoldingDecl (← getEnv) declName || !(← isRecursiveDefinition declName) then
       d := d.addDeclToUnfoldCore declName
     return d
   else