# Documentation

Init.Data.Format.Basic

Determines how groups should have linebreaks inserted when the text would overfill its remaining space.

• allOrNone will make a linebreak on every Format.line in the group or none of them.
[1,
2,
3]

• fill will only make linebreaks on as few Format.lines as possible:
[1, 2,
3]

Instances For
Equations
inductive Std.Format :
• The empty format.

nil: Lean.Format
• A position where a newline may be inserted if the current group does not fit within the allotted column width.

line: Lean.Format
• align tells the formatter to pad with spaces to the current indent, or else add a newline if we are already at or past the indent. For example:

nest 2 <| "." ++ align ++ "a" ++ line ++ "b"


results in:

. a
b


If force is true, then it will pad to the indent even if it is in a flattened group.

align:
• A node containing a plain string.

text:
• nest n f tells the formatter that f is nested inside something with length n so that it is pretty-printed with the correct indentation on a line break. For example, we can define a formatter for list l : List Format as:

let f := join <| l.intersperse <| ", " ++ Format.line
group (nest 1 <| "[" ++ f ++ "]")


This will be written all on one line, but if the text is too large, the formatter will put in linebreaks after the commas and indent later lines by 1.

nest:
• Concatenation of two Formats.

append:
• Creates a new flattening group for the given inner format.

group:
• Used for associating auxiliary information (e.g. Exprs) with Format objects.

tag:

A string with pretty-printing information for rendering in a column-width-aware way.

The pretty-printing algorithm is based on Wadler's paper A Prettier Printer.

Instances For

Check whether the given format contains no characters.

Equations

Alias for a group with FlattenBehavior set to fill.

Equations
Equations
Equations
Equations
• = match x with | Lean.Format.nil => true | x => false
Equations
• pushOutput : Stringm Unit
• pushNewline : Natm Unit
• currColumn : m Nat
• Start a scope tagged with n.

startTag : Natm Unit
• Exit the scope of n-many opened tags.

endTags : Natm Unit

A monad in which we can pretty-print Format objects.

Instances
def Std.Format.prettyM {m : } (f : Lean.Format) (w : Nat) (indent : ) [inst : ] [inst : ] :

Render the given f : Format with a line width of w. indent is the starting amount to indent each line by.

Equations
@[inline]

Create a format l ++ f ++ r with a flatten group. FlattenBehaviour is allOrNone; for fill use bracketFill.

Equations
@[inline]

Creates the format "(" ++ f ++ ")" with a flattening group.

Equations
@[inline]

Creates the format "[" ++ f ++ "]" with a flattening group.

Equations
@[inline]

Same as bracket except uses the fill flattening behaviour.

Equations

Default indentation.

Equations
Equations

Default width of the targeted output pane.

Equations

Nest with the default indentation amount.

Equations

Insert a newline and then f, all nested by the default indent amount.

Equations
Equations
• One or more equations did not get rendered due to their size.
@[export lean_format_pretty]

Pretty-print a Format object as a string with expected width w.

Equations
• = let act := ; (act { out := "", column := 0 }).snd.out
class Std.ToFormat (α : Type u) :
• format :

Class for converting a given type α to a Format object for pretty-printing. See also Repr, which also outputs a Format object.

Instances
Equations
Equations
def Std.Format.joinSep {α : Type u} [inst : ] :

Intersperse the given list (each item printed with format) with the given sep format.

Equations
def Std.Format.prefixJoin {α : Type u} [inst : ] (pre : Lean.Format) :

Format each item in items and prepend prefix pre.

Equations
def Std.Format.joinSuffix {α : Type u} [inst : ] :

Format each item in items and append suffix.

Equations