def
Lean.Elab.Structural.mkIndPredBRecOn
(recArgInfo : Lean.Elab.Structural.RecArgInfo)
(value : Lean.Expr)
:
Transform the body of a recursive function into a non-recursive one.
The value is the function with (only) the fixed parameters instantiated.
Equations
- One or more equations did not get rendered due to their size.