mathlib documentation

core.init.data.repr

@[class]
structure has_repr  :
Type uType 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
@[instance]

Equations
@[instance]
def decidable.has_repr {p : Prop} :

Equations
def list.repr_aux {α : Type u} [has_repr α] :
boollist αstring

Equations
def list.repr {α : Type u} [has_repr α] :
list αstring

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

Equations
@[instance]

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

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

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

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

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

Equations
def nat.digit_char  :
char

Equations
def nat.digit_succ  :
list list

Equations
def nat.to_digits  :
list

Equations
@[instance]

Equations
def char_to_hex  :

Equations

Equations
@[instance]

Equations
def string.quote  :

Equations
@[instance]
def fin.has_repr (n : ) :

Equations
@[instance]

Equations
def char.repr  :

Equations