chore(library/init/data): add missing instances
This commit is contained in:
parent
13ba9ca176
commit
ba633df7e7
2 changed files with 6 additions and 0 deletions
|
|
@ -125,6 +125,9 @@ else "\"" ++ string.quote_aux s.to_list ++ "\""
|
|||
instance : has_repr string :=
|
||||
⟨string.quote⟩
|
||||
|
||||
instance : has_repr string.iterator :=
|
||||
⟨λ it, it.next_to_string.quote ++ ".mk_iterator"⟩
|
||||
|
||||
instance (n : nat) : has_repr (fin n) :=
|
||||
⟨λ f, repr (fin.val f)⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -20,6 +20,9 @@ has_to_string.to_string
|
|||
instance : has_to_string string :=
|
||||
⟨λ s, s⟩
|
||||
|
||||
instance : has_to_string string.iterator :=
|
||||
⟨λ it, it.next_to_string⟩
|
||||
|
||||
instance : has_to_string bool :=
|
||||
⟨λ b, cond b "tt" "ff"⟩
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue