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.