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 : Lean.Name
• openDecls : List Lean.OpenDecl

@[reducible, inline]

abbrev Lean.PrettyPrinter.InfoPerPos : Type

Equations

• Lean.PrettyPrinter.InfoPerPos = Lean.RBMap Nat Lean.Elab.Info compare

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 : Lean.Format
• infos : Lean.PrettyPrinter.InfoPerPos

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

Equations

• Lean.instCoeFormatFormatWithInfos = { coe := fun (fmt : Lean.Format) => { fmt := fmt, infos := ∅ } }

structure Lean.PPFns : Type

• ppExprWithInfos : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos
• ppConstNameWithInfos : Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos
• ppTerm : Lean.PPContext → Lean.Term → IO Lean.Format
• ppLevel : Lean.PPContext → Lean.Level → 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.ppConstNameWithInfos (ctx : Lean.PPContext) (n : Lean.Name) : IO Lean.FormatWithInfos

Equations

• Lean.ppConstNameWithInfos ctx n = (Lean.ppExt.getState ctx.env).ppConstNameWithInfos ctx n

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

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

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