def Lean.mkRecAppWithSyntax (e : Expr) (stx : Syntax) : Expr

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 : Expr) : Option Syntax

Retrieve (if available) the syntax object attached to a recursive application.

def Lean.MData.isRecApp (d : MData) : Bool

Checks if the MData is for a recursive application.

def Lean.hasRecAppSyntax (e : Expr) : Bool

Return true if getRecAppSyntax? e is a some.