source
opaque Lean.pp.raw :
Lean.Option Bool
source
opaque Lean.pp.raw.showInfo :
Lean.Option Bool
source
opaque Lean.pp.raw.maxDepth :
Lean.Option Nat
source
opaque Lean.pp.rawOnError :
Lean.Option Bool
source
structure Lean.PPContext :
Type

- env : Environment
- mctx : MetavarContext
- lctx : LocalContext
- opts : Options
- currNamespace : Name
- openDecls : List OpenDecl

Instances For

source
@[reducible, inline]
abbrev Lean.PrettyPrinter.InfoPerPos :
Type
Equations

- Lean.PrettyPrinter.InfoPerPos = Std.TreeMap Nat Lean.Elab.Info compare

Instances For

source
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

Instances For

source
instance Lean.instCoeFormatFormatWithInfos :
Coe Format FormatWithInfos
Equations

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

source
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

Instances For

source
instance Lean.instInhabitedPPFns :
Inhabited PPFns
Equations

- Lean.instInhabitedPPFns = { default := Lean.instInhabitedPPFns.default }

source
def Lean.instInhabitedPPFns.default :
PPFns
Equations

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

Instances For

source
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)

Instances For

source
def Lean.formatRawGoal (mvarId : MVarId) :
Format
Equations

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

Instances For

source
opaque Lean.ppFnsRef :
IO.Ref PPFns
source
opaque Lean.ppExt :
EnvExtension PPFns
source
def Lean.ppExprWithInfos (ctx : PPContext) (e : Expr) :
BaseIO FormatWithInfos
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For