def Lean.PPContext.runCoreM {α : Type} (ppCtx : Lean.PPContext) (x : Lean.CoreM α) : IO α

Equations

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

def Lean.PPContext.runMetaM {α : Type} (ppCtx : Lean.PPContext) (x : Lean.MetaM α) : IO α

Equations

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

def Lean.PrettyPrinter.ppCategory (cat : Lake.Name) (stx : Lean.Syntax) : Lean.CoreM Lean.Format

Equations

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

def Lean.PrettyPrinter.ppTerm (stx : Lean.Term) : Lean.CoreM Lean.Format

Equations

• Lean.PrettyPrinter.ppTerm stx = Lean.PrettyPrinter.ppCategory `term stx.raw

def Lean.PrettyPrinter.ppUsing (e : Lean.Expr) (delab : Lean.Expr → Lean.MetaM Lean.Term) : Lean.MetaM Lean.Format

Equations

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

def Lean.PrettyPrinter.ppExpr (e : Lean.Expr) : Lean.MetaM Lean.Format

Equations

• Lean.PrettyPrinter.ppExpr e = Lean.PrettyPrinter.ppUsing e fun e => Lean.PrettyPrinter.delab e ∅

def Lean.PrettyPrinter.ppExprWithInfos (e : Lean.Expr) (optsPerPos : optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅) (delab : optParam Lean.PrettyPrinter.Delaborator.Delab Lean.PrettyPrinter.Delaborator.delab) : Lean.MetaM Lean.FormatWithInfos

Return a fmt representing pretty-printed e together with a map from tags in fmt to Elab.Info nodes produced by the delaborator at various subexpressions of e.

Equations

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

def Lean.PrettyPrinter.ppConst (e : Lean.Expr) : Lean.MetaM Lean.Format

Equations

• Lean.PrettyPrinter.ppConst e = Lean.PrettyPrinter.ppUsing e fun e => do let __do_lift ← Lean.PrettyPrinter.delabCore e ∅ Lean.PrettyPrinter.Delaborator.delabConst pure __do_lift.fst

@[export lean_pp_expr]

def Lean.PrettyPrinter.ppExprLegacy (env : Lean.Environment) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (opts : Lean.Options) (e : Lean.Expr) : IO Lean.Format

Equations

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

def Lean.PrettyPrinter.ppTactic (stx : Lean.TSyntax `tactic) : Lean.CoreM Lean.Format

Equations

• Lean.PrettyPrinter.ppTactic stx = Lean.PrettyPrinter.ppCategory `tactic stx.raw

def Lean.PrettyPrinter.ppCommand (stx : Lean.Command) : Lean.CoreM Lean.Format

Equations

• Lean.PrettyPrinter.ppCommand stx = Lean.PrettyPrinter.ppCategory `command stx.raw

def Lean.PrettyPrinter.ppModule (stx : Lean.TSyntax `Lean.Parser.Module.module) : Lean.CoreM Lean.Format

Equations

• Lean.PrettyPrinter.ppModule stx = Lean.PrettyPrinter.parenthesize Lean.Parser.Module.module.parenthesizer stx.raw >>= Lean.PrettyPrinter.format Lean.Parser.Module.module.formatter

def Lean.PrettyPrinter.ppSignature (c : Lake.Name) : Lean.MetaM Lean.FormatWithInfos

Pretty-prints a declaration c as c.{} : .

Equations

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

unsafe def Lean.PrettyPrinter.registerParserCompilers : IO Unit

Equations

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