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

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

Equations

• Lean.instCoeFormatFormatWithInfos = { coe := fun (fmt : Std.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 Std.Format
• ppLevel : Lean.PPContext → Lean.Level → BaseIO Std.Format
• ppGoal : Lean.PPContext → Lean.MVarId → IO Std.Format

instance Lean.instInhabitedPPFns : Inhabited Lean.PPFns

Equations

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

def Lean.formatRawTerm (ctx : Lean.PPContext) (stx : Lean.Term) : Std.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 : Lean.MVarId) : Std.Format

Equations

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

opaque Lean.ppFnsRef : IO.Ref Lean.PPFns

opaque Lean.ppExt : Lean.EnvExtension Lean.PPFns

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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