def Lean.mkRecAppWithSyntax (e : Lean.Expr) (stx : Lean.Syntax) : Lean.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 : Lean.Expr) : Option Lean.Syntax

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

Equations

• Lean.getRecAppSyntax? (Lean.Expr.mdata d expr) = match Lean.KVMap.find d Lean.recAppKey✝ with | some (Lean.DataValue.ofSyntax stx) => some stx | x => none
• Lean.getRecAppSyntax? e = none

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

Checks if the MData is for a recursive application.

def Lean.hasRecAppSyntax (e : Lean.Expr) : Bool

Return true if getRecAppSyntax? e is a some.

Equations

• Lean.hasRecAppSyntax (Lean.Expr.mdata d expr) = d.isRecApp
• Lean.hasRecAppSyntax e = false