Documentation

Lean.Elab.PreDefinition.Structural.Preprocess

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

def f : NatNat
  | 0 => 1
  | i+1 => (fun x => f x) i
Instances For