def Lean.mkRecAppWithSyntax (e : Lean.Expr) (stx : Lean.Syntax) :
We store the syntax at recursive applications to be able to generate better error messages when performing well-founded and structural recursion.
def Lean.getRecAppSyntax? (e : Lean.Expr) :
Retrieve (if available) the syntax object attached to a recursive application.
- One or more equations did not get rendered due to their size.