Documentation

Lean.Util.PPExt

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

structure Lean.PPFns:

Type

ppExpr : Lean.PPContext → Lean.Expr → IO Lean.Format
ppTerm : Lean.PPContext → Lean.Syntax → IO Lean.Format
ppGoal : Lean.PPContext → Lean.MVarId → IO Lean.Format

instance Lean.instInhabitedPPFns:

Inhabited Lean.PPFns

Equations

Lean.instInhabitedPPFns = { default := { ppExpr := default, ppTerm := default, ppGoal := default } }

opaque Lean.ppFnsRef:

IO.Ref Lean.PPFns

opaque Lean.ppExt:

Lean.EnvExtension Lean.PPFns

def Lean.ppExpr (ctx : Lean.PPContext) (e : Lean.Expr) :

Equations

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

def Lean.ppTerm (ctx : Lean.PPContext) (stx : Lean.Syntax) :

Equations

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

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

Equations

Lean.ppGoal ctx mvarId = Lean.PPFns.ppGoal (Lean.EnvExtension.getState Lean.ppExt ctx.env) ctx mvarId