From 21d94096299fe387da36cea12c79cfd50d7b2913 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Apr 2018 13:23:07 -0700 Subject: [PATCH] feat(library/init/data): modify unit `has_to_string` and `has_repr` instances --- library/init/data/repr.lean | 2 +- library/init/data/to_string.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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⟩