mathlib documentation

core / init.data.to_string

@[class]
structure has_to_string (α : Type u) :
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
def to_string {α : Type u} [has_to_string α] :
α → string
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
def list.to_string {α : Type u} [has_to_string α] :
list αstring
Equations
@[protected, instance]
def list.has_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]
def option.has_to_string {α : Type u} [has_to_string α] :
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