Documentation

Lean.Util.PPExt

constant Lean.pp.raw :

Lean.Option Bool

constant Lean.pp.raw.showInfo :

Lean.Option Bool

constant Lean.pp.raw.maxDepth :

Lean.Option Nat

constant 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 } }

constant Lean.ppFnsRef :

IO.Ref Lean.PPFns

constant Lean.ppExt :

Lean.EnvExtension Lean.PPFns

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

Equations

Lean.ppExpr ctx e = let e := (Lean.MetavarContext.instantiateMVars ctx.mctx e).fst; if Lean.Option.get ctx.opts Lean.pp.raw = true then pure (Lean.format (toString e)) else tryCatch (Lean.PPFns.ppExpr (Lean.EnvExtension.getState Lean.ppExt ctx.env) ctx e) fun ex => if Lean.Option.get ctx.opts Lean.pp.rawOnError = true then pure (Lean.format "[Error pretty printing expression: " ++ Lean.format ex ++ Lean.format ". Falling back to raw printer.]" ++ Lean.format Lean.Format.line ++ Lean.format "" ++ Lean.format e ++ Lean.format "") else pure (Lean.format "failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)")

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

Equations

Lean.ppTerm ctx stx = let fmtRaw := fun x => Lean.Syntax.formatStx stx (some (Lean.Option.get ctx.opts Lean.pp.raw.maxDepth)) (Lean.Option.get ctx.opts Lean.pp.raw.showInfo); if Lean.Option.get ctx.opts Lean.pp.raw = true then pure (fmtRaw ()) else tryCatch (Lean.PPFns.ppTerm (Lean.EnvExtension.getState Lean.ppExt ctx.env) ctx stx) fun ex => if Lean.Option.get ctx.opts Lean.pp.rawOnError = true then pure (Lean.format "[Error pretty printing syntax: " ++ Lean.format ex ++ Lean.format ". Falling back to raw printer.]" ++ Lean.format Lean.Format.line ++ Lean.format "" ++ Lean.format (fmtRaw ()) ++ Lean.format "") else pure (Lean.format "failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)")

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