mathlib docs: core.init.data.repr

@[class]

structure has_repr :

Type u → Type u

repr : α → string

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

source

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

repr = has_repr.repr

source

@[instance]

def bool.has_repr :

has_repr bool

Equations

bool.has_repr = {repr := λ (b : bool), cond b "tt" "ff"}

source

@[instance]

def decidable.has_repr {p : Prop} :

has_repr (decidable p)

Equations

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

source

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

bool → list α → string

Equations

list.repr_aux bool.tt (x :: xs) = repr x ++ list.repr_aux bool.ff xs
list.repr_aux bool.tt list.nil = ""
list.repr_aux bool.ff (x :: xs) = ", " ++ repr x ++ list.repr_aux bool.ff xs
list.repr_aux bool.ff list.nil = ""

source

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

list α → string

Equations

(x :: xs).repr = "[" ++ list.repr_aux bool.tt (x :: xs) ++ "]"
list.nil.repr = "[]"

source

@[instance]

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

has_repr (list α)

Equations

list.has_repr = {repr := list.repr _inst_1}

source

@[instance]

def unit.has_repr :

has_repr unit

Equations

unit.has_repr = {repr := λ (u : unit), "star"}

source

@[instance]

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

has_repr (option α)

Equations

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

source

@[instance]

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

has_repr (α ⊕ β)

Equations

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

source

@[instance]

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

has_repr (α × β)

Equations

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

source

@[instance]

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

has_repr (sigma β)

Equations

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

source

@[instance]

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

has_repr (subtype p)

Equations

subtype.has_repr = {repr := λ (s : subtype p), repr s.val}

source

def nat.digit_char :

ℕ → char

Equations

n.digit_char = ite (n = 0) '0' (ite (n = 1) '1' (ite (n = 2) '2' (ite (n = 3) '3' (ite (n = 4) '4' (ite (n = 5) '5' (ite (n = 6) '6' (ite (n = 7) '7' (ite (n = 8) '8' (ite (n = 9) '9' (ite (n = 10) 'a' (ite (n = 11) 'b' (ite (n = 12) 'c' (ite (n = 13) 'd' (ite (n = 14) 'e' (ite (n = 15) 'f' '*')))))))))))))))

source

def nat.digit_succ :

ℕ → list ℕ → list ℕ

Equations

base.digit_succ (d :: ds) = ite (d + 1 = base) (0 :: base.digit_succ ds) ((d + 1) :: ds)
base.digit_succ list.nil = [1]

source

def nat.to_digits :

ℕ → ℕ → list ℕ

Equations

base.to_digits (n + 1) = base.digit_succ (base.to_digits n)
base.to_digits 0 = [0]

source

def nat.repr :

ℕ → string

Equations

n.repr = (list.map nat.digit_char (10.to_digits n)).reverse.as_string

source

@[instance]

def nat.has_repr :

has_repr ℕ

Equations

nat.has_repr = {repr := nat.repr}

source

def hex_digit_repr :

ℕ → string

Equations

hex_digit_repr n = string.singleton n.digit_char

source

def char_to_hex :

char → string

Equations

char_to_hex c = let n : ℕ := c.to_nat, d2 : ℕ := n / 16, d1 : ℕ := n % 16 in hex_digit_repr d2 ++ hex_digit_repr d1

source

def char.quote_core :

char → string

Equations

c.quote_core = ite (c = '\n') "\\n" (ite (c = '\t') "\\t" (ite (c = '\\') "\\\\" (ite (c = '"') "\\\"" (ite (c.to_nat ≤ 31 ∨ c = '\x7f') ("\\x" ++ char_to_hex c) (string.singleton c)))))