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
Retrieve (if available) the syntax object attached to a recursive application.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Checks if the MData
is for a recursive applciation.
Equations
- d.isRecApp = Lean.KVMap.contains d Lean.recAppKey