We store the syntax at recursive applications to be able to generate better error messages when performing well-founded and structural recursion.
Instances For
Retrieve (if available) the syntax object attached to a recursive application.
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.
Retrieve (if available) the syntax object attached to a recursive application.