@[class]
- to_string : α → string
Convert the object into a string for tracing/display purposes.
Similar to Haskell's show.
See also has_repr, which is used to output a string which is a valid lean code.
See also has_to_format and has_to_tactic_format, format has additional support for colours and pretty printing multilines.
Instances
- string.has_to_string
- bool.has_to_string
- decidable.has_to_string
- list.has_to_string
- unit.has_to_string
- nat.has_to_string
- char.has_to_string
- fin.has_to_string
- unsigned.has_to_string
- option.has_to_string
- sum.has_to_string
- prod.has_to_string
- sigma.has_to_string
- subtype.has_to_string
- name.has_to_string
- format.has_to_string
- exceptional.has_to_string
- level.has_to_string
- native.has_to_string
- expr.has_to_string
- interaction_monad.result_has_string
- tactic_state.has_to_string
- tactic.interactive.case_tag.has_to_string
- module_info.has_to_string
- expr.coord.has_to_string
- expr.address.has_to_string
- widget.interactive_expression.has_to_string
- int.has_to_string
- native.float.has_to_string
- tactic_doc_entry.has_to_string
- binder.has_to_string
- widget_override.interactive_expression.has_to_string
- norm_cast.label.has_to_string
- tactic.has_to_string
- tactic.tactic_script_unit_has_to_string
- rat.has_to_string
- linarith.ineq.has_to_string
- omega.term.has_to_string
- composition.has_to_string
- expr_lens.has_to_string
- erased.has_to_string
- hash_map.has_to_string
- onote.has_to_string
- nonote.has_to_string
- side.has_to_string
- tactic.ring2.horner_expr.has_to_string
Equations
@[instance]
Equations
- string.has_to_string = {to_string := λ (s : string), s}
@[instance]
@[instance]
Equations
- list.to_string_aux bool.tt (x :: xs) = to_string x ++ list.to_string_aux bool.ff xs
- list.to_string_aux bool.tt list.nil = ""
- list.to_string_aux bool.ff (x :: xs) = ", " ++ to_string x ++ list.to_string_aux bool.ff xs
- list.to_string_aux bool.ff list.nil = ""
@[instance]
Equations
- list.has_to_string = {to_string := list.to_string _inst_1}
@[instance]
Equations
- unit.has_to_string = {to_string := λ (u : unit), "star"}
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
Equations
- option.has_to_string = {to_string := λ (o : option α), option.has_to_string._match_1 o}
- option.has_to_string._match_1 (option.some a) = "(some " ++ to_string a ++ ")"
- option.has_to_string._match_1 option.none = "none"
@[instance]
def
sum.has_to_string
{α : Type u}
{β : Type v}
[has_to_string α]
[has_to_string β] :
has_to_string (α ⊕ β)
@[instance]
def
prod.has_to_string
{α : Type u}
{β : Type v}
[has_to_string α]
[has_to_string β] :
has_to_string (α × β)
@[instance]
def
sigma.has_to_string
{α : Type u}
{β : α → Type v}
[has_to_string α]
[s : Π (x : α), has_to_string (β x)] :
has_to_string (sigma β)
@[instance]
def
subtype.has_to_string
{α : Type u}
{p : α → Prop}
[has_to_string α] :
has_to_string (subtype p)