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

Equations

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

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

Equations

• Std.Format.instBEqFlattenBehavior = { beq := Std.Format.beqFlattenBehavior✝ }

inductive Std.Format : Type

• 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

• A node containing a plain string.

  text: String → 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.

  nest: Int → Lean.Format → Lean.Format

• Concatenation of two Formats.

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

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

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

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

  tag: Nat → Lean.Format → Lean.Format

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

Equations

• Std.instInhabitedFormat = { default := Lean.Format.nil }

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

Equations

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

@[export lean_format_append]

def Std.Format.appendEx (a : Lean.Format) (b : Lean.Format) : Lean.Format

Equations

• Std.Format.appendEx a b = Std.Format.append a b

@[export lean_format_group]

def Std.Format.groupEx : Lean.Format → Lean.Format

Equations

• Std.Format.groupEx a = Lean.Format.group a

instance Std.Format.instAppendFormat : Append Lean.Format

Equations

• Std.Format.instAppendFormat = { append := Std.Format.append }

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

Equations

• Std.Format.instCoeStringFormat = { coe := Std.Format.text }

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

Equations

• Lean.Format.join xs = List.foldl (fun a a_1 => a ++ a_1) (Std.Format.text "") xs

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

Equations

• Std.Format.isNil _fun_discr = match _fun_discr with | Lean.Format.nil => true | x => false

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

Equations

• Std.Format.instInhabitedSpaceResult = { default := { foundLine := default, foundFlattenedHardLine := default, space := default } }

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

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

• Start a scope tagged with n.

  startTag : Nat → m Unit

• Exit the scope of n-many opened tags.

  endTags : Nat → m Unit

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) [inst : Monad m] [inst : 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

• Std.Format.prettyM f w indent = Std.Format.be w [{ flatten := false, flb := Std.Format.FlattenBehavior.allOrNone, items := [{ f := f, indent := Int.ofNat 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.group (Lean.Format.nest (Int.ofNat (String.length l)) (Std.Format.text l ++ f ++ Std.Format.text r))

@[inline]

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

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

Equations

• Lean.Format.paren f = Lean.Format.bracket "(" f ")"

@[inline]

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

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

Equations

• Lean.Format.sbracket f = 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.

Equations

• Std.Format.bracketFill l f r = Lean.Format.fill (Lean.Format.nest (Int.ofNat (String.length l)) (Std.Format.text l ++ f ++ Std.Format.text r))

def Std.Format.defIndent : Nat

Default indentation.

Equations

• Std.Format.defIndent = 2

def Std.Format.defUnicode : Bool

Equations

• Std.Format.defUnicode = true

def Std.Format.defWidth : Nat

Default width of the targeted output pane.

Equations

• Std.Format.defWidth = 120

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

Nest with the default indentation amount.

Equations

• Std.Format.nestD f = Lean.Format.nest (Int.ofNat 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

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

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) (w : optParam Nat Std.Format.defWidth) : String

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

Equations

• Lean.Format.pretty f w = let act := Std.Format.prettyM f w 0; (act { out := "", column := 0 }).snd.out

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

Equations

• Std.instToFormatFormat = { format := fun f => f }

instance Std.instToFormatString : Lean.ToFormat String

Equations

• Std.instToFormatString = { format := fun s => Std.Format.text s }

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

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

Equations

• Lean.Format.joinSep [] _fun_discr = Lean.Format.nil
• Lean.Format.joinSep [a] _fun_discr = Lean.format a
• Lean.Format.joinSep (a :: as) _fun_discr = Lean.format a ++ _fun_discr ++ Lean.Format.joinSep as _fun_discr

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

Format each item in items and prepend prefix pre.

Equations

• Std.Format.prefixJoin pre [] = Lean.Format.nil
• Std.Format.prefixJoin pre (a :: as) = pre ++ Lean.format a ++ Std.Format.prefixJoin pre as

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

Format each item in items and append suffix.

Equations

• Std.Format.joinSuffix [] _fun_discr = Lean.Format.nil
• Std.Format.joinSuffix (a :: as) _fun_discr = Lean.format a ++ _fun_discr ++ Std.Format.joinSuffix as _fun_discr