def Lean.PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α

def Lean.PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α

def Lean.PrettyPrinter.ppCategory (cat : Name) (stx : Syntax) : CoreM Format

def Lean.PrettyPrinter.ppTerm (stx : Term) : CoreM Format

def Lean.PrettyPrinter.ppUsing (e : Expr) (delab : Expr → MetaM Term) : MetaM Format

opaque Lean.PrettyPrinter.pp.exprSizes : Lean.Option Bool

def Lean.PrettyPrinter.ppExpr (e : Expr) : MetaM Format

def Lean.PrettyPrinter.ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := ∅) (delab : Delaborator.Delab := Delaborator.delab) : MetaM FormatWithInfos

Return a fmt representing pretty-printed e together with a map from tags in fmt to Elab.Info nodes produced by the delaborator at various subexpressions of e.

def Lean.PrettyPrinter.ppConstNameWithInfos (constName : Name) : MetaM FormatWithInfos

@[export lean_pp_expr]

def Lean.PrettyPrinter.ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format

def Lean.PrettyPrinter.ppTactic (stx : TSyntax `tactic) : CoreM Format

def Lean.PrettyPrinter.ppCommand (stx : Command) : CoreM Format

def Lean.PrettyPrinter.ppModule (stx : TSyntax `Lean.Parser.Module.module) : CoreM Format

def Lean.PrettyPrinter.ppSignature (c : Name) : MetaM FormatWithInfos

Pretty-prints a declaration c as c.{<levels>} <params> : <type>.

unsafe def Lean.PrettyPrinter.registerParserCompilers : IO Unit

def Lean.MessageData.ofFormatWithInfosM (fmt : MetaM FormatWithInfos) : MessageData

Turns a MetaM FormatWithInfos into a MessageData.lazy which will run the monadic value.

def Lean.MessageData.ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData

Turns a MetaM MessageData into a MessageData.lazy which will run the monadic value. The optional array of expressions is used to set the hasSyntheticSorry fields, and should comprise the expressions that are included in the message data.

def Lean.MessageData.ofConst (e : Expr) : MessageData

Pretty print a const expression using delabConst and generate terminfo. This function avoids inserting @ if the constant is for a function whose first argument is implicit, which is what the default toMessageData for Expr does. Panics if e is not a constant.

def Lean.MessageData.signature (c : Name) : MessageData

Generates MessageData for a declaration c as c.{<levels>} <params> : <type>, with terminfo.