mathlib3 documentation

core / init.meta.format

inductive format.color :

red : format.color
green : format.color
orange : format.color
blue : format.color
pink : format.color
cyan : format.color
grey : format.color

Instances for format.color

format.color.has_sizeof_inst
format.color.inhabited

def format.color.to_string :

format.color → string

Equations

format.color.grey.to_string = "grey"
format.color.cyan.to_string = "cyan"
format.color.pink.to_string = "pink"
format.color.blue.to_string = "blue"
format.color.orange.to_string = "orange"
format.color.green.to_string = "green"
format.color.red.to_string = "red"

meta constant format :

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

Instances for format

meta constant format.line :

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

meta constant format.space :

The whitespace character " ".

meta constant format.nil :

= ""

meta constant format.compose :

format → format → format

Concatenate the given format strings.

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.

meta constant format.highlight :

format → format.color → format

Make the given format be displayed a particular color.

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.

meta constant format.of_string :

string → format

meta constant format.of_nat :

meta constant format.flatten :

format → format

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

meta constant format.to_string (f : format) (o : options := options.mk) :

meta constant format.of_options :

options → format

meta constant format.is_nil :

format → bool

meta constant trace_fmt {α : Type u} :

format → (unit → α) → α

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

@[protected, instance]

meta def format.inhabited :

inhabited format

@[protected, instance]

meta def format.has_append :

has_append format

@[protected, instance]

meta def format.has_to_string :

has_to_string format

@[class]

meta structure has_to_format (α : Type u) :

to_format : α → format

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 of this typeclass

@[protected, instance]

meta def format.has_to_format :

has_to_format format

meta def to_fmt {α : Type u} [has_to_format α] :

@[protected, instance]

meta def nat_to_format :

has_coe ℕ format

@[protected, instance]

meta def string_to_format :

has_coe string format

meta def format.indent (f : format) (n : ℕ) :

meta def format.when {α : Type u} [has_to_format α] :

bool → α → format

meta def format.join (xs : list format) :

@[protected, instance]

meta def options.has_to_format :

has_to_format options

@[protected, instance]

meta def bool.has_to_format :

has_to_format bool

@[protected, instance]

meta def decidable.has_to_format {p : Prop} :

has_to_format (decidable p)

@[protected, instance]

meta def string.has_to_format :

has_to_format string

@[protected, instance]

meta def nat.has_to_format :

has_to_format ℕ

@[protected, instance]

meta def unsigned.has_to_format :

has_to_format unsigned

@[protected, instance]

meta def char.has_to_format :

has_to_format char

meta def list.to_format {α : Type u} [has_to_format α] :

list α → format

@[protected, instance]

meta def list.has_to_format {α : Type u} [has_to_format α] :

has_to_format (list α)

@[protected, instance]

meta def name.has_to_format :

has_to_format name

@[protected, instance]

meta def unit.has_to_format :

has_to_format unit

@[protected, instance]

meta def option.has_to_format {α : Type u} [has_to_format α] :

has_to_format (option α)

@[protected, instance]

meta def sum_has_to_format {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] :

has_to_format (α ⊕ β)

@[protected, instance]

meta def prod.has_to_format {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] :

has_to_format (α × β)

@[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 β)

@[protected, instance]

meta def subtype.has_to_format {α : Type u} {p : α → Prop} [has_to_format α] :

has_to_format (subtype p)

meta def format.bracket :

string → string → format → format

meta def format.paren (f : format) :

Surround with "()".

meta def format.cbrace (f : format) :

Surround with "{}".

meta def format.sbracket (f : format) :

Surround with "[]".

meta def format.dcbrace (f : format) :

Surround with "⦃⦄".