Documentation

Lean.Elab.RecAppSyntax

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

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

Equations

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