source
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.

Equations

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

Instances For

source
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

Instances For

source
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✝

Instances For

source
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

Instances For