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
    Instances For

      Checks if the MData is for a recursive application.

      Equations
      Instances For

        Return true if getRecAppSyntax? e is a some.

        Equations
        Instances For