mathlib3 documentation

core / init.meta.format

inductive format.color  :
Instances for 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'.

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  :

= ""

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

Make the given format be displayed a particular color.

meta constant format.group  :

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_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 := options.mk) :
meta constant format.is_nil  :
meta constant trace_fmt {α : Type u} :

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[class]
meta structure has_to_format (α : 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 of this typeclass
@[protected, instance]
meta def to_fmt {α : Type u} [has_to_format α] :
@[protected, instance]
@[protected, instance]
meta def format.indent (f : format) (n : ) :
meta def format.when {α : Type u} [has_to_format α] :
meta def format.join (xs : list format) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
meta def decidable.has_to_format {p : Prop} :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
meta def list.to_format {α : Type u} [has_to_format α] :
@[protected, instance]
meta def list.has_to_format {α : Type u} [has_to_format α] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
meta def sum_has_to_format {α : Type u} {β : Type v} [has_to_format α] [has_to_format β] :
@[protected, instance]
meta def prod.has_to_format {α : Type u} {β : Type v} [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)] :
@[protected, instance]
meta def subtype.has_to_format {α : Type u} {p : α Prop} [has_to_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 "⦃⦄".