- allOrNone: Std.Format.FlattenBehavior
- fill: Std.Format.FlattenBehavior
Determines how groups should have linebreaks inserted when the text would overfill its remaining space.
allOrNonewill make a linebreak on everyFormat.linein the group or none of them.[1, 2, 3]fillwill only make linebreaks on as fewFormat.lines as possible:[1, 2, 3]
Instances For
- 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
- text: String → Lean.Format
A node containing a plain string.
- nest: Int → Lean.Format → Lean.Format
nest n ftells the formatter thatfis nested inside something with lengthnso that it is pretty-printed with the correct indentation on a line break. For example, we can define a formatter for listl : List Formatas: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) withFormatobjects.
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
- 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
Instances For
Alias for a group with FlattenBehavior set to fill.
Instances For
Render the given f : Format with a line width of w.
indent is the starting amount to indent each line by.
Instances For
Create a format l ++ f ++ r with a flatten group.
FlattenBehaviour is allOrNone; for fill use bracketFill.
Instances For
Creates the format "(" ++ f ++ ")" with a flattening group.
Instances For
Creates the format "[" ++ f ++ "]" with a flattening group.
Instances For
Nest with the default indentation amount.
Instances For
Insert a newline and then f, all nested by the default indent amount.
Instances For
Pretty-print a Format object as a string with expected width w.
Instances For
- 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.
Instances
Intersperse the given list (each item printed with format) with the given sep format.
Instances For
Format each item in items and prepend prefix pre.
Instances For
Format each item in items and append suffix.