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

Preprocesses the expessions to improve the effectiveness of elimRecursion.

• Beta reduce terms where the recursive function occurs in the lambda term. Example:

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

• Floats out the RecApp markers. Example:

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

Equations

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