mathlib documentation

core / init.meta.format

source
inductive format.color  :
Type
source
def format.color.to_string  :
format.color → string
Equations
source
meta constant format  :
Type

Format is a rich string with highlighting and information about how tabs should be put in if linebreaks are needed. A 'pretty string'.

source
meta constant format.line  :
format

Indicate that it is ok to put a linebreak in here if the line is too long.

source
meta constant format.space  :
format

The whitespace character " ".

source
meta constant format.nil  :
format

= ""

source
meta constant format.compose  :
format → format → format

Concatenate the given format strings.

source
meta constant format.nest  :
ℕ → format → format

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 tabs on a line break. For example, in list.to_format we have:

(nest 1 $ format.join $ list.intersperse ("," ++ line) $ xs.map to_fmt)

This will be written all on one line, but when the list is too large, it will put in linebreaks after the comma and indent later lines by 1.

source
meta constant format.highlight  :
format → format.color → format

Make the given format be displayed a particular color.

source
meta constant format.group  :
format → format

When printing the given format f, if f.flatten fits without need for linebreaks then print the f.flatten, else print f unflattened with linebreaks.

source
meta constant format.of_string  :
string → format
source
meta constant format.of_nat  :
ℕ → format
source
meta constant format.flatten  :
format → format

Flattening removes all of the format.nest items from the format tree.

source
meta constant format.to_string (f : format) (o : options := options.mk) :
string
source
meta constant format.of_options  :
options → format
source
meta constant format.is_nil  :
format → bool
source
meta constant trace_fmt {α : Type u} :
format → (unit → α) → α

Traces the given format to the output window, then performs the given continuation.

source
@[protected, instance]
meta def format.inhabited  :
inhabited format
source
@[protected, instance]
meta def format.has_append  :
has_append format
source
@[protected, instance]
meta def format.has_to_string  :
has_to_string format
source
@[class]
meta structure has_to_format (α : Type u) :
Type u

Use this instead of has_to_string to enable prettier formatting. See docstring for format for more on the differences between format and string. Note that format is meta while string is not.

Instances
source
@[protected, instance]
meta def format.has_to_format  :
has_to_format format
source
meta def to_fmt {α : Type u} [has_to_format α] :
α → format
source
@[protected, instance]
meta def nat_to_format  :
has_coe ℕ format
source
@[protected, instance]
meta def string_to_format  :
has_coe string format
source
meta def format.indent (f : format) (n : ℕ) :
format
source
meta def format.when {α : Type u} [has_to_format α] :
bool → α → format
source
meta def format.join (xs : list format) :
format
source
@[protected, instance]
meta def options.has_to_format  :
has_to_format options
source
@[protected, instance]
meta def bool.has_to_format  :
has_to_format bool
source
@[protected, instance]
meta def decidable.has_to_format {p : Prop} :
has_to_format (decidable p)
source
@[protected, instance]
meta def string.has_to_format  :
has_to_format string
source
@[protected, instance]
meta def nat.has_to_format  :
has_to_format ℕ
source
@[protected, instance]
meta def unsigned.has_to_format  :
has_to_format unsigned
source
@[protected, instance]
meta def char.has_to_format  :
has_to_format char
source
meta def list.to_format {α : Type u} [has_to_format α] :
list α → format
source
@[protected, instance]
meta def list.has_to_format {α : Type u} [has_to_format α] :
has_to_format (list α)
source
@[protected, instance]
meta def name.has_to_format  :
has_to_format name
source
@[protected, instance]
meta def unit.has_to_format  :
has_to_format unit
source
@[protected, instance]
meta def option.has_to_format {α : Type u} [has_to_format α] :
has_to_format (option α)
source
@[protected, instance]
meta def sum_has_to_format {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] :
has_to_format (α ⊕ β)
source
@[protected, instance]
meta def prod.has_to_format {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] :
has_to_format (α × β)
source
@[protected, instance]
meta def sigma.has_to_format {α : Type u} {β : α → Type v} [has_to_format α] [s : Π (x : α), has_to_format (β x)] :
has_to_format (sigma β)
source
@[protected, instance]
meta def subtype.has_to_format {α : Type u} {p : α → Prop} [has_to_format α] :
has_to_format (subtype p)
source
meta def format.bracket  :
string → string → format → format
source
meta def format.paren (f : format) :
format

Surround with "()".

source
meta def format.cbrace (f : format) :
format

Surround with "{}".

source
meta def format.sbracket (f : format) :
format

Surround with "[]".

source
meta def format.dcbrace (f : format) :
format

Surround with "⦃⦄".