opaque Lean.PrettyPrinter.backtrackExceptionId : InternalExceptionId

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

Equations

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