mathlib documentation

core / init.meta.format

inductive format.color  :

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

meta constant format.line  :

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

meta constant  :

The whitespace character " ".

meta constant format.nil  :

= ""

meta constant format.compose  :

Concatenate the given format strings.

meta constant format.nest  :

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) $ 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  :

Make the given format be displayed a particular color.

meta constant  :

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  :

meta constant format.of_nat  :

meta constant format.flatten  :

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

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

meta constant format.of_options  :

meta constant format.is_nil  :

meta constant trace_fmt {α : Type u} :
format(unit → α) → α

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




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.


meta def to_fmt {α : Type u} [has_to_format α] :
α → 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) :


meta def decidable.has_to_format {p : Prop} :




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

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



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

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

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

meta def sigma.has_to_format {α : Type u} {β : α → Type v} [has_to_format α] [s : Π (x : α), has_to_format (β x)] :

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

meta def format.bracket  :

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 "⦃⦄".