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 : Environment
• mctx : MetavarContext
• lctx : LocalContext
• opts : Options
• currNamespace : Name
• openDecls : List OpenDecl

@[reducible, inline]

abbrev Lean.PrettyPrinter.InfoPerPos : Type

structure Lean.FormatWithInfos : Type

A format tree with Elab.Info annotations. Each .tag n _ node is annotated with infos[n]. This is used to attach semantic data such as expressions to pretty-printer outputs.

• fmt : Format
• infos : PrettyPrinter.InfoPerPos

instance Lean.instCoeFormatFormatWithInfos : Coe Format FormatWithInfos

structure Lean.PPFns : Type

• ppExprWithInfos : PPContext → Expr → IO FormatWithInfos
• ppConstNameWithInfos : PPContext → Name → IO FormatWithInfos
• ppTerm : PPContext → Term → IO Format
• ppLevel : PPContext → Level → BaseIO Format
• ppGoal : PPContext → MVarId → IO Format

instance Lean.instInhabitedPPFns : Inhabited PPFns

def Lean.formatRawTerm (ctx : PPContext) (stx : Term) : Format

def Lean.formatRawGoal (mvarId : MVarId) : Format

opaque Lean.ppFnsRef : IO.Ref PPFns

opaque Lean.ppExt : EnvExtension PPFns

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

def Lean.ppConstNameWithInfos (ctx : PPContext) (n : Name) : BaseIO FormatWithInfos

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

def Lean.ppLevel (ctx : PPContext) (l : Level) : BaseIO Format

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