Documentation

Lean.PrettyPrinter

source
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.
source
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.
source
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.
source
def Lean.PrettyPrinter.ppTerm (stx : Lean.Term) :
Lean.CoreM Lean.Format
Equations
source
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.
source
opaque Lean.PrettyPrinter.pp.exprSizes :
Lean.Option Bool
source
def Lean.PrettyPrinter.ppExpr (e : Lean.Expr) :
Lean.MetaM Lean.Format
Equations
source
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.
source
@[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.
source
def Lean.PrettyPrinter.ppTactic (stx : Lean.TSyntax `tactic) :
Lean.CoreM Lean.Format
Equations
source
def Lean.PrettyPrinter.ppCommand (stx : Lean.Command) :
Lean.CoreM Lean.Format
Equations
source
def Lean.PrettyPrinter.ppModule (stx : Lean.TSyntax `Lean.Parser.Module.module) :
Lean.CoreM Lean.Format
Equations
source
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.
source
unsafe def Lean.PrettyPrinter.registerParserCompilers :
IO Unit
source
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.

Equations
source
def Lean.MessageData.ofLazyM (f : Lean.MetaM Lean.MessageData) (es : optParam (Array Lean.Expr) #[]) :
Lean.MessageData

Turns a MetaM MessageData into a MessageData.lazy which will run the monadic value. The optional array of expressions is used to set the hasSyntheticSorry fields, and should comprise the expressions that are included in the message data.

Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
def Lean.MessageData.ofConstName (constName : Lake.Name) :
Lean.MessageData

Pretty print a constant given its name, similar to Lean.MessageData.ofConst. Uses the constant's universe level parameters when pretty printing. If there is no such constant in the environment, the name is simply formatted.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MessageData.signature (c : Lake.Name) :
Lean.MessageData

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

Equations