def Lean.Elab.Structural.preprocess (e : Lean.Expr) (recFnName : Lake.Name) : Lean.CoreM Lean.Expr

Beta reduce terms where the recursive function occurs in the lambda term. This is useful to improve the effectiveness of elimRecursion. Example:

def f : Nat → Nat
  | 0 => 1
  | i+1 => (fun x => f x) i

Equations

• One or more equations did not get rendered due to their size.