opaque Lean.pp.raw : Lean.Option Bool

opaque Lean.pp.raw.showInfo : Lean.Option Bool

opaque Lean.pp.raw.maxDepth : Lean.Option Nat

opaque Lean.pp.rawOnError : Lean.Option Bool

structure Lean.PPContext : Type

• env : Lean.Environment
• mctx : Lean.MetavarContext
• lctx : Lean.LocalContext
• opts : Lean.Options
• currNamespace : Lake.Name
• openDecls : List Lean.OpenDecl

@[inline, reducible]

abbrev Lean.PrettyPrinter.InfoPerPos : Type

structure Lean.FormatWithInfos : Type

• fmt : Lean.Format
• infos : Lean.PrettyPrinter.InfoPerPos

instance Lean.instCoeFormatFormatWithInfos : Coe Lean.Format Lean.FormatWithInfos

structure Lean.PPFns : Type

• ppExprWithInfos : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos
• ppTerm : Lean.PPContext → Lean.Term → IO Lean.Format
• ppGoal : Lean.PPContext → Lean.MVarId → IO Lean.Format

instance Lean.instInhabitedPPFns : Inhabited Lean.PPFns

opaque Lean.ppFnsRef : IO.Ref Lean.PPFns

opaque Lean.ppExt : Lean.EnvExtension Lean.PPFns

def Lean.ppExprWithInfos (ctx : Lean.PPContext) (e : Lean.Expr) : IO Lean.FormatWithInfos

def Lean.ppTerm (ctx : Lean.PPContext) (stx : Lean.Term) : IO Lean.Format

def Lean.ppGoal (ctx : Lean.PPContext) (mvarId : Lean.MVarId) : IO Lean.Format