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

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

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

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

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

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

def Lean.PrettyPrinter.ppExprWithInfos (e : Lean.Expr) (optsPerPos : optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅) (delab : optParam Lean.PrettyPrinter.Delaborator.Delab Lean.PrettyPrinter.Delaborator.delab) : Lean.MetaM Lean.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.ppConst (e : Lean.Expr) : Lean.MetaM Lean.Format

@[export lean_pp_expr]

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

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

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

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

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

Pretty-prints a declaration c as c.{} : .

unsafe def Lean.PrettyPrinter.registerParserCompilers : IO Unit