mathlib documentation

core.​init.​meta.​format

core.​init.​meta.​format

inductive format.​color  :
Type

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

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  :

Concatenate the given format strings.

meta constant format.​nest  :
formatformat

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  :

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_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.​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.

@[instance]

@[instance]

@[class]
meta structure has_to_format  :
Type uType 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
meta def to_fmt {α : Type u} [has_to_format α] :
α → format

@[instance]

@[instance]

meta def format.​indent  :
formatformat

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

@[instance]

@[instance]

@[instance]

@[instance]

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

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

@[instance]

@[instance]

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

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

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

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

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

meta def format.​bracket  :

meta def format.​paren  :

Surround with "()".

meta def format.​cbrace  :

Surround with "{}".

meta def format.​sbracket  :

Surround with "[]".

meta def format.​dcbrace  :

Surround with "⦃⦄".