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

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.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.