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.ofFormatWithInfosM (fmt : Lean.MetaM Lean.FormatWithInfos) : Lean.MessageData

Turns a MetaM FormatWithInfos into a MessageData.lazy which will run the monadic value. 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.ofFormatWithInfosM (Lean.PrettyPrinter.ppSignature c)