# Documentation

Lean.PrettyPrinter.Formatter

The formatter turns a Syntax tree into a Format object, inserting both mandatory whitespace (to separate adjacent tokens) as well as "pretty" optional whitespace.

The basic approach works much like the parenthesizer: A right-to-left traversal over the syntax tree, driven by parser-specific handlers registered via attributes. The traversal is right-to-left so that when emitting a token, we already know the text following it and can decide whether or not whitespace between the two is necessary.

Instances For
@[inline]
Equations
@[inline]
def Lean.PrettyPrinter.FormatterM.orElse {α : Type} (p₁ : ) (p₂ : ) :
Equations
Equations
• Lean.PrettyPrinter.instOrElseFormatterM = { orElse := Lean.PrettyPrinter.FormatterM.orElse }
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• Lean.PrettyPrinter.Formatter.throwBacktrack =
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations

Execute x at the right-most child of the current node, if any, then advance to the left.

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

Execute x, pass array of generated Format objects to fn, and push result.

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

Execute x and concatenate generated Format objects.

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

If pos? has a position, run x and tag its results with that position, if they are not already tagged. Otherwise just run x.

Equations
• One or more equations did not get rendered due to their size.
@[extern lean_mk_antiquot_formatter]
@[extern lean_pretty_printer_formatter_interpret_parser_descr]
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by Lean.PrettyPrinter.Formatter.formatterForKindUnsafe]
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
@[macro_inline]
def Lean.PrettyPrinter.Formatter.ite :
{x : Type} → (c : Prop) →
Equations
• = if c then t else e
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations