Documentation

Lean.Elab.PreDefinition.Structural.Preprocess

Preprocesses the expressions to improve the effectiveness of elimRecursion.

  • Beta reduce terms where the recursive function occurs in the lambda term. Example:
def f : NatNat
  | 0 => 1
  | i+1 => (fun x => f x) i
  • Floats out the RecApp markers. Example:
def f : NatNat
  | 0 => 1
  | i+1 => (f x) i
Equations
  • One or more equations did not get rendered due to their size.
Instances For