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

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

instance Lean.instCoeFormatFormatWithInfos : Coe Format FormatWithInfos

Equations

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

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

Equations

• Lean.instInhabitedPPFns = { default := { ppExprWithInfos := default, ppConstNameWithInfos := default, ppTerm := default, ppLevel := default, ppGoal := default } }

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

Equations

• Lean.formatRawTerm ctx stx = stx.raw.formatStx (some (Lean.Option.get ctx.opts Lean.pp.raw.maxDepth)) (Lean.Option.get ctx.opts Lean.pp.raw.showInfo)

def Lean.formatRawGoal (mvarId : MVarId) : Format

Equations

• Lean.formatRawGoal mvarId = Std.Format.text "goal " ++ Std.format (Lean.mkMVar mvarId)

opaque Lean.ppFnsRef : IO.Ref PPFns

opaque Lean.ppExt : EnvExtension PPFns

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.ppLevel ctx l = (Lean.ppExt.getState ctx.env).ppLevel ctx l

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

Equations

• One or more equations did not get rendered due to their size.