mathlib documentation

core / init.data.repr

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

Implement has_repr if the output string is valid lean code that evaluates back to the original object. If you just want to view the object as a string for a trace message, use has_to_string.

Example: #

#eval to_string "hello world"
-- [Lean] "hello world"
#eval repr "hello world"
-- [Lean] "\"hello world\""

Reference: https://github.com/leanprover/lean/issues/1664

Instances
def repr {α : Type u} [has_repr α] :
α → string

repr is similar to to_string except that we should have the property eval (repr x) = x for most sensible datatypes. Hence, repr "hello" has the value "\"hello\"" not "hello".

Equations
@[protected, instance]
Equations
@[protected, instance]
def decidable.has_repr {p : Prop} :
Equations
@[protected]
def list.repr_aux {α : Type u} [has_repr α] :
boollist αstring
Equations
@[protected]
def list.repr {α : Type u} [has_repr α] :
list αstring
Equations
@[protected, instance]
def list.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def option.has_repr {α : Type u} [has_repr α] :
Equations
@[protected, instance]
def sum.has_repr {α : Type u} {β : Type v} [has_repr α] [has_repr β] :
has_repr β)
Equations
@[protected, instance]
def prod.has_repr {α : Type u} {β : Type v} [has_repr α] [has_repr β] :
has_repr × β)
Equations
@[protected, instance]
def sigma.has_repr {α : Type u} {β : α → Type v} [has_repr α] [s : Π (x : α), has_repr (β x)] :
Equations
@[protected, instance]
def subtype.has_repr {α : Type u} {p : α → Prop} [has_repr α] :
Equations
def nat.digit_char (n : ) :
Equations
def nat.digit_succ (base : ) :
Equations
def nat.to_digits (base : ) :
Equations
@[protected]
def nat.repr (n : ) :
Equations
@[protected, instance]
Equations
def char_to_hex (c : char) :
Equations
def char.quote_core (c : char) :
Equations
@[protected, instance]
Equations
def string.quote (s : string) :
Equations
@[protected, instance]
Equations
@[protected, instance]
def fin.has_repr (n : ) :
Equations
@[protected, instance]
Equations
def char.repr (c : char) :
Equations