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.

We additionally store the source position as an extra key, so that two recursive applications that are structurally identical as Syntax but originate from different source positions still produce distinct MData. Otherwise hashconsing or simplification can merge them and attribute an error to the wrong call site (issue #13444).

Equations

• One or more equations did not get rendered due to their size.

def Lean.getRecAppSyntax? (e : Expr) : Option 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 : MData) : Bool

Checks if the MData is for a recursive application.

Equations

• d.isRecApp = Lean.KVMap.contains d Lean.recAppKey✝

def Lean.hasRecAppSyntax (e : Expr) : Bool

Return true if getRecAppSyntax? e is a some.

Equations

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