opaque Lean.PrettyPrinter.backtrackExceptionId : Lean.InternalExceptionId

unsafe def Lean.PrettyPrinter.runForNodeKind {α : Type} (attr : Lean.KeyedDeclsAttribute α) (k : Lean.SyntaxNodeKind) (interp : Lean.ParserDescr → Lean.CoreM α) : Lean.CoreM α

Equations

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