max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/data): modify unit has_to_string and has_repr instances

Browse source
This commit is contained in:
Leonardo de Moura 2018-04-27 13:23:07 -07:00
parent 3f812698a9
commit 21d9409629
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/data/repr.lean
View file

@ -36,7 +36,7 @@ instance {α : Type u} [has_repr α] : has_repr (list α) :=
⟨list.repr⟩
instance : has_repr unit :=
⟨λ u, "star"⟩
⟨λ u, "()"⟩
instance {α : Type u} [has_repr α] : has_repr (option α) :=
⟨λ o, match o with | none := "none" | (some a) := "(some " ++ repr a ++ ")" end⟩

2
library/init/data/to_string.lean
View file

@ -43,7 +43,7 @@ instance {α : Type u} [has_to_string α] : has_to_string (list α) :=
⟨list.to_string⟩
instance : has_to_string unit :=
⟨λ u, "star"⟩
⟨λ u, "()"⟩
instance : has_to_string nat :=
⟨λ n, repr n⟩