From ba633df7e74b97d403df2672b6c5fcd4c71d7366 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Apr 2018 10:30:06 -0700 Subject: [PATCH] chore(library/init/data): add missing instances --- library/init/data/repr.lean | 3 +++ library/init/data/to_string.lean | 3 +++ 2 files changed, 6 insertions(+) diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean index 565e8faa10..c739189f80 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.lean @@ -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)⟩ diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean index fc1e27943a..544f0769ba 100644 --- a/library/init/data/to_string.lean +++ b/library/init/data/to_string.lean @@ -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"⟩