mathlib3 documentation

core / init.data.to_string

@[class]
structure has_to_string (α : Type u) :

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 of this typeclass
Instances of other typeclasses for has_to_string
  • has_to_string.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
def list.to_string {α : Type u} [has_to_string α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def sum.has_to_string {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] :
Equations
@[protected, instance]
def prod.has_to_string {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] :
Equations
@[protected, instance]
def sigma.has_to_string {α : Type u} {β : α Type v} [has_to_string α] [s : Π (x : α), has_to_string (β x)] :
Equations
@[protected, instance]
def subtype.has_to_string {α : Type u} {p : α Prop} [has_to_string α] :
Equations