mathlib documentation

core / init.data.to_string

@[class]

structure has_to_string (α : Type u) :

Type u

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

def to_string {α : Type u} [has_to_string α] :

α → string

Equations

to_string = has_to_string.to_string

@[protected, instance]

def string.has_to_string :

has_to_string string

Equations

string.has_to_string = {to_string := λ (s : string), s}

@[protected, instance]

def bool.has_to_string :

has_to_string bool

Equations

bool.has_to_string = {to_string := λ (b : bool), cond b "tt" "ff"}

@[protected, instance]

def decidable.has_to_string {p : Prop} :

has_to_string (decidable p)

Equations

decidable.has_to_string = {to_string := λ (b : decidable p), ite p "tt" "ff"}

@[protected]

def list.to_string_aux {α : Type u} [has_to_string α] :

bool → list α → string

Equations

list.to_string_aux tt (x :: xs) = to_string x ++ list.to_string_aux ff xs
list.to_string_aux tt list.nil = ""
list.to_string_aux ff (x :: xs) = ", " ++ to_string x ++ list.to_string_aux ff xs
list.to_string_aux ff list.nil = ""

@[protected]

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

list α → string

Equations

(x :: xs).to_string = "[" ++ list.to_string_aux tt (x :: xs) ++ "]"
list.nil.to_string = "[]"

@[protected, instance]

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

has_to_string (list α)

Equations

list.has_to_string = {to_string := list.to_string _inst_1}

@[protected, instance]

def unit.has_to_string :

has_to_string unit

Equations

unit.has_to_string = {to_string := λ (u : unit), "star"}

@[protected, instance]

def nat.has_to_string :

has_to_string ℕ

Equations

nat.has_to_string = {to_string := λ (n : ℕ), repr n}

@[protected, instance]

def char.has_to_string :

has_to_string char

Equations

char.has_to_string = {to_string := λ (c : char), c.to_string}

@[protected, instance]

def fin.has_to_string (n : ℕ) :

has_to_string (fin n)

Equations

fin.has_to_string n = {to_string := λ (f : fin n), to_string f.val}

@[protected, instance]

def unsigned.has_to_string :

has_to_string unsigned

Equations

unsigned.has_to_string = {to_string := λ (n : unsigned), to_string n.val}

@[protected, instance]

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

has_to_string (option α)

Equations

option.has_to_string = {to_string := λ (o : option α), option.has_to_string._match_1 o}
option.has_to_string._match_1 (some a) = "(some " ++ to_string a ++ ")"
option.has_to_string._match_1 none = "none"

@[protected, instance]

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

has_to_string (α ⊕ β)

Equations

sum.has_to_string = {to_string := λ (s : α ⊕ β), sum.has_to_string._match_1 s}
sum.has_to_string._match_1 (sum.inr b) = "(inr " ++ to_string b ++ ")"
sum.has_to_string._match_1 (sum.inl a) = "(inl " ++ to_string a ++ ")"

@[protected, instance]

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

has_to_string (α × β)

Equations

prod.has_to_string = {to_string := λ (_x : α × β), prod.has_to_string._match_1 _x}
prod.has_to_string._match_1 (a, b) = "(" ++ to_string a ++ ", " ++ to_string b ++ ")"

@[protected, instance]

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

has_to_string (sigma β)

Equations

sigma.has_to_string = {to_string := λ (_x : sigma β), sigma.has_to_string._match_1 _x}
sigma.has_to_string._match_1 ⟨a, b⟩ = "⟨" ++ to_string a ++ ", " ++ to_string b ++ "⟩"

@[protected, instance]

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

has_to_string (subtype p)

Equations

subtype.has_to_string = {to_string := λ (s : subtype p), to_string s.val}