Documentation

Lean.Elab.RecAppSyntax

We store the syntax at recursive applications to be able to generate better error messages when performing well-founded and structural recursion.

Equations
Instances For

    Retrieve (if available) the syntax object attached to a recursive application.

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

      Checks if the MData is for a recursive applciation.

      Equations
      Instances For