← Copula mathematical handbook

structure Lean.PPContext : Type

Saved context for pretty printing. See Lean.ppExt.

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