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

Equations

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

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

Equations

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

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

Equations

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

opaque Lean.PrettyPrinter.pp.exprSizes : Lean.Option Bool

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

Equations

• Lean.PrettyPrinter.ppExpr e = (Lean.PrettyPrinter.ppUsing e fun (e : Lean.Expr) => Lean.PrettyPrinter.delab e) >>= Lean.PrettyPrinter.maybePrependExprSizes✝ e

def Lean.PrettyPrinter.ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := ∅) (delab : Delaborator.Delab := Delaborator.delab) : MetaM 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.ppConstNameWithInfos (constName : Name) : MetaM FormatWithInfos

Equations

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

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

Equations

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

def Lean.PrettyPrinter.ppLevel (l : Level) : MetaM Format

Equations

• Lean.PrettyPrinter.ppLevel l = do let __do_lift ← Lean.PrettyPrinter.delabLevel l 0 liftM (Lean.PrettyPrinter.ppCategory `level __do_lift.raw)

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

Equations

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

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

Equations

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

def Lean.PrettyPrinter.ppModule (stx : TSyntax `Lean.Parser.Module.module) : CoreM 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 : Name) : MetaM FormatWithInfos

Pretty-prints a declaration c as c.{<levels>} <params> : <type>.

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.

def Lean.MessageData.ofFormatWithInfosM (fmt : MetaM FormatWithInfos) : MessageData

Turns a MetaM FormatWithInfos into a MessageData.lazy which will run the monadic value.

Equations

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

def Lean.MessageData.ofConst (e : Expr) : MessageData

Pretty print a const expression using delabConst and generate terminfo. This function avoids inserting @ if the constant is for a function whose first argument is implicit, which is what the default toMessageData for Expr does. Panics if e is not a constant.

Equations

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

def Lean.MessageData.signature (c : Name) : MessageData

Generates MessageData for a declaration c as c.{<levels>} <params> : <type>, with terminfo.

Equations

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