inductive Std.Format.FlattenBehavior : Type

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]
  

• allOrNone: Std.Format.FlattenBehavior
• fill: Std.Format.FlattenBehavior

instance Std.Format.instInhabitedFlattenBehavior : Inhabited Std.Format.FlattenBehavior

Equations

• Std.Format.instInhabitedFlattenBehavior = { default := Std.Format.FlattenBehavior.allOrNone }

instance Std.Format.instBEqFlattenBehavior : BEq Std.Format.FlattenBehavior

inductive Std.Format : Type

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.

• nil: Lean.Format

  The empty format.

• line: Lean.Format

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

• align: Bool → 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.

• text: String → Lean.Format

  A node containing a plain string.

• nest: Int → Lean.Format → Lean.Format

  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.

• append: Lean.Format → Lean.Format → Lean.Format

  Concatenation of two Formats.

• group: Lean.Format → optParam Std.Format.FlattenBehavior Std.Format.FlattenBehavior.allOrNone → Lean.Format

  Creates a new flattening group for the given inner format.

• tag: Nat → Lean.Format → Lean.Format

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

instance Std.instInhabitedFormat : Inhabited Lean.Format

def Std.Format.isEmpty : Lean.Format → Bool

Check whether the given format contains no characters.

Equations

• Lean.Format.nil.isEmpty = true
• Lean.Format.line.isEmpty = false
• (Lean.Format.align force).isEmpty = true
• (Std.Format.text msg).isEmpty = (msg == "")
• (Lean.Format.nest indent f).isEmpty = f.isEmpty
• (f₁.append f₂).isEmpty = (f₁.isEmpty && f₂.isEmpty)
• (f.group behavior).isEmpty = f.isEmpty
• (Lean.Format.tag a f).isEmpty = f.isEmpty

def Std.Format.fill (f : Lean.Format) : Lean.Format

Alias for a group with FlattenBehavior set to fill.

Equations

• f.fill = f.group Std.Format.FlattenBehavior.fill

instance Std.Format.instAppend : Append Lean.Format

instance Std.Format.instCoeString : Coe String Lean.Format

def Std.Format.join (xs : List Lean.Format) : Lean.Format

def Std.Format.isNil : Lean.Format → Bool

Equations

• Lean.Format.nil.isNil = true
• x.isNil = false

instance Std.Format.instInhabitedSpaceResult : Inhabited Std.Format.SpaceResult✝

class Std.Format.MonadPrettyFormat (m : Type → Type) : Type

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

• pushOutput : String → m Unit
• pushNewline : Nat → m Unit
• currColumn : m Nat
• startTag : Nat → m Unit

  Start a scope tagged with n.

• endTags : Nat → m Unit

  Exit the scope of n-many opened tags.

def Std.Format.prettyM {m : Type → Type} (f : Lean.Format) (w : Nat) (indent : Nat := 0) [Monad m] [Std.Format.MonadPrettyFormat m] : m Unit

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

Equations

• f.prettyM w indent = Std.Format.be✝ w [{ flatten := false, flb := Std.Format.FlattenBehavior.allOrNone, items := [{ f := f, indent := ↑indent, activeTags := 0 }] }]

@[inline]

def Std.Format.bracket (l : String) (f : Lean.Format) (r : String) : Lean.Format

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

Equations

• Lean.Format.bracket l f r = (Lean.Format.nest (↑l.length) (Std.Format.text l ++ f ++ Std.Format.text r)).group

@[inline]

def Std.Format.paren (f : Lean.Format) : Lean.Format

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

@[inline]

def Std.Format.sbracket (f : Lean.Format) : Lean.Format

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

Equations

• f.sbracket = Lean.Format.bracket "[" f "]"

@[inline]

def Std.Format.bracketFill (l : String) (f : Lean.Format) (r : String) : Lean.Format

Same as bracket except uses the fill flattening behaviour.

def Std.Format.defIndent : Nat

Default indentation.

Equations

• Std.Format.defIndent = 2

def Std.Format.defUnicode : Bool

def Std.Format.defWidth : Nat

Default width of the targeted output pane.

def Std.Format.nestD (f : Lean.Format) : Lean.Format

Nest with the default indentation amount.

Equations

• f.nestD = Lean.Format.nest (↑Std.Format.defIndent) f

def Std.Format.indentD (f : Lean.Format) : Lean.Format

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

Equations

• f.indentD = (Lean.Format.line ++ f).nestD

instance Std.Format.instMonadPrettyFormatStateMState : Std.Format.MonadPrettyFormat (StateM Std.Format.State✝)

Equations

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

@[export lean_format_pretty]

def Std.Format.pretty (f : Lean.Format) (width : Nat := Std.Format.defWidth) (indent column : Nat := 0) : String

Renders a Format to a string.

• width: the total width
• indent: the initial indentation to use for wrapped lines (subsequent wrapping may increase the indentation)
• column: begin the first line wrap column characters earlier than usual (this is useful when the output String will be printed starting at column)

class Std.ToFormat (α : Type u) : Type u

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

• format : α → Lean.Format

instance Std.instToFormatFormat : Lean.ToFormat Lean.Format

instance Std.instToFormatString : Lean.ToFormat String

def Std.Format.joinSep {α : Type u} [Lean.ToFormat α] : List α → Lean.Format → Lean.Format

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

def Std.Format.prefixJoin {α : Type u} [Lean.ToFormat α] (pre : Lean.Format) : List α → Lean.Format

Format each item in items and prepend prefix pre.

Equations

• pre.prefixJoin [] = Lean.Format.nil
• pre.prefixJoin (a :: as) = List.foldl (fun (x1 : Lean.Format) (x2 : α) => x1 ++ pre ++ Lean.format x2) (pre ++ Lean.format a) as

def Std.Format.joinSuffix {α : Type u} [Lean.ToFormat α] : List α → Lean.Format → Lean.Format

Format each item in items and append suffix.

Equations

• Std.Format.joinSuffix [] x = Lean.Format.nil
• Std.Format.joinSuffix (a :: as) x = List.foldl (fun (x1 : Lean.Format) (x2 : α) => x1 ++ Lean.format x2 ++ x) (Lean.format a ++ x) as