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.

Equations

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