Lean.Elab.PreDefinition.Structural.Preprocess
source
Beta reduce terms where the recursive function occurs in the lambda term. This is useful to improve the effectiveness of elimRecursion. Example:
elimRecursion
def f : Nat → Nat | 0 => 1 | i+1 => (fun x => f x) i