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