inductive Std.Format.FlattenBehavior : Type

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

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]
  

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

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

inductive Std.Format : Type

• 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.

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.

instance Std.instInhabitedFormat : Inhabited Lean.Format

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

Check whether the given format contains no characters.

Equations

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

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

Alias for a group with FlattenBehavior set to fill.

instance Std.Format.instAppendFormat : Append Lean.Format

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

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

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

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

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

• 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.

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

def Std.Format.prettyM {m : Type → Type} (f : Lean.Format) (w : Nat) (indent : optParam 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.

@[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.

@[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.

@[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.

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.

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

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

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

@[export lean_format_pretty]

def Std.Format.pretty (f : Lean.Format) (w : optParam Nat Std.Format.defWidth) : String

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

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

• format : α → Lean.Format

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

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.

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

Format each item in items and append suffix.