mathlib documentation

core.init.data.to_string

@[class]
structure has_to_string  :
Type uType 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
def to_string {α : Type u} [has_to_string α] :
α → string

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
def list.to_string {α : Type u} [has_to_string α] :
list αstring

Equations
@[instance]
def list.has_to_string {α : Type u} [has_to_string α] :

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]
def option.has_to_string {α : Type u} [has_to_string α] :

Equations
@[instance]
def sum.has_to_string {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] :

Equations
@[instance]
def prod.has_to_string {α : Type u} {β : Type v} [has_to_string α] [has_to_string β] :

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

Equations
@[instance]
def subtype.has_to_string {α : Type u} {p : α → Prop} [has_to_string α] :

Equations