diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean index c739189f80..1229cd56e9 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.lean @@ -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⟩ diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean index 544f0769ba..04f0c3788b 100644 --- a/library/init/data/to_string.lean +++ b/library/init/data/to_string.lean @@ -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⟩