- red : format.color
- green : format.color
- orange : format.color
- blue : format.color
- pink : format.color
- cyan : format.color
- grey : format.color
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"
Indicate that it is ok to put a linebreak in here if the line is too long.
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.
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.
Flattening removes all of the format.nest items from the format tree.
- 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
- format.has_to_format
- options.has_to_format
- bool.has_to_format
- decidable.has_to_format
- nat.has_to_format
- unsigned.has_to_format
- char.has_to_format
- list.has_to_format
- string.has_to_format
- name.has_to_format
- unit.has_to_format
- option.has_to_format
- sum_has_to_format
- prod.has_to_format
- sigma.has_to_format
- subtype.has_to_format
- level.has_to_format
- native.has_to_format
- native.rb_set.has_to_format
- name_set.has_to_format
- pos.has_to_format
- expr.has_to_format
- reflected.has_to_format
- tactic_state.has_to_format
- occurrences.has_to_format
- congr_arg_kind.has_to_format
- tactic.interactive.case_tag.has_to_format
- param_info.has_to_format
- fun_info.has_to_format
- subsingleton_info.has_to_format
- local_context.has_to_format
- module_info.has_to_format
- expr.coord.has_to_format
- expr.address.has_to_format
- tagged_format.has_to_fmt
- widget.interactive_expression.has_to_format
- array.has_to_format
- native.float.has_to_format
- doc_category.has_to_format
- binder.has_to_format
- widget_override.interactive_expression.has_to_format
- buffer.has_to_format
- norm_cast.label.has_to_format
- with_bot.has_to_format
- with_top.has_to_format
- int.has_to_format
- tactic.interactive.has_to_format
- rat.has_to_format
- linarith.ineq.has_to_format
- linarith.comp.to_format
- linarith.comp_source.has_to_format
- linarith.pcomp.to_format
- omega.ee.has_to_format
- omega.int.preform.has_to_format
- omega.nat.preform.has_to_format
- erased.has_to_format
- hash_map.has_to_format