def Lean.Elab.Structural.mkIndPredBRecOn (recArgInfo : RecArgInfo) (value : Expr) : M Expr

Transform the body of a recursive function into a non-recursive one.

The value is the function with (only) the fixed parameters instantiated.