Documentation

Lean.Elab.RecAppSyntax

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.

Equations

Lean.mkRecAppWithSyntax e stx = Lean.mkMData (Lean.KVMap.insert Lean.KVMap.empty Lean.recAppKey (Lean.DataValue.ofSyntax stx)) e

def Lean.getRecAppSyntax? (e : Lean.Expr) :

Option Lean.Syntax

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

Equations

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