Documentation

Lean.Elab.PreDefinition.WF.Preprocess

Preprocesses the expressions to improve the effectiveness of wfRecursion.

  • Floats out the RecApp markers. Example:
    def f : NatNat
      | 0 => 1
      | i+1 => (f x) i
    

Unlike Lean.Elab.Structural.preprocess, do not beta-reduce, as it could remove let_fun-lambdas that contain explicit termination proofs.

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