source
def Lean.Elab.WF.floatRecApp (e : Expr) :
CoreM Expr

Preprocesses the expressions to improve the effectiveness of `wfRecursion`.

- Floats out the RecApp markers. Example:

      def f : Nat → Nat
        | 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. (Note(kmill): this last statement no longer affects `let_fun`/`have`.)

Equations

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

Instances For