fix: nested structural recursion

src/Lean/Elab/PreDefinition/Structural.lean

@@ -231,8 +231,12 @@ let rec loop : Expr → Expr → MetaM Expr
           -- Recall that the fixed parameters are not in the scope of the `brecOn`. So, we skip them.
           let argsNonFixed := args.extract numFixed args.size
           -- The function `f` does not explicitly take `recArg` and its indices as arguments. So, we skip them too.
-          let fArgs := argsNonFixed.iterate #[] fun i a fArgs =>
-            if recArgInfo.pos == i.val || recArgInfo.indicesPos.contains i.val then fArgs else fArgs.push a
+          let fArgs := #[]
+          for i in [:argsNonFixed.size] do
+            if recArgInfo.pos != i && !recArgInfo.indicesPos.contains i then
+              let arg := argsNonFixed[i]
+              let arg ← replaceRecApps recFnName recArgInfo below arg
+              fArgs := fArgs.push arg
           pure $ mkAppN f fArgs
         else
           pure $ mkAppN (← loop below f) (← args.mapM (loop below))

tests/lean/run/nestedrec.lean

@@ -0,0 +1,12 @@
+#lang lean4
+
+def f : Nat → Nat → Nat
+| 0,   b => b+1
+| a+1, b => f a (f a b)
+
+theorem ex1 (b)   : f 0 b = b+1 := rfl
+theorem ex2 (b)   : f 1 b = (b+1)+1 := rfl
+theorem ex3 (b)   : f 2 b = b+1+1+1+1 := rfl
+theorem ex4 (a b) : f (a+1) b = f a (f a b) := rfl
+
+#eval f 2 5