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.Expr) => 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.

@[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.{<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.ofFormatWithInfos (fmt : Lean.MetaM Lean.FormatWithInfos) (noContext : optParam (Unit → Lean.Format) fun (x : Unit) => Std.Format.text "<no context, could not generate MessageData>") : Lean.MessageData

Turns a MetaM FormatWithInfos into a MessageData using .ofPPFormat and running the monadic value in the given context. Uses the pp.tagAppFns option to annotate constants with terminfo, which is necessary for seeing the type on mouse hover.

Equations

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

def Lean.MessageData.ofConst (e : Lean.Expr) : Lean.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 : Lake.Name) : Lean.MessageData

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

Equations

• Lean.MessageData.signature c = Lean.MessageData.ofFormatWithInfos (Lean.PrettyPrinter.ppSignature c) fun (x : Unit) => Std.format "" ++ Std.format c ++ Std.format ""