From 039f1de524293c86b1ce7a88e612e9636b11ba91 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Apr 2015 21:26:56 -0700
Subject: [PATCH] fix(library/data/countable): typos

---
 library/data/countable.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/data/countable.lean b/library/data/countable.lean
index b84ba71a7..512468c8e 100644
--- a/library/data/countable.lean
+++ b/library/data/countable.lean
@@ -68,7 +68,7 @@ theorem unpickle_pickle_sum : ∀ s : sum A B, unpickle_sum (pickle_sum s) = som
              mul_div_cancel_left _ aux₁, countable.picklek]
   end
 
-definition countable_sum [instance] {A B : Type} [h₁ : countable A] [h₂ : countable B] : countable (sum A B) :=
+definition countable_sum [instance] : countable (sum A B) :=
 countable.mk
   (λ s, pickle_sum s)
   (λ n, unpickle_sum n)
@@ -105,7 +105,7 @@ theorem unpickle_pickle_prod : ∀ p : A × B, unpickle_prod (pickle_prod p) = s
     rewrite [*countable.picklek]
   end
 
-definition countable_product [instance] {A B : Type} [h₁ : countable A] [h₂ : countable B] : countable (A × B) :=
+definition countable_product [instance] : countable (A × B) :=
 countable.mk
   pickle_prod
   unpickle_prod
@@ -181,7 +181,7 @@ begin
   apply unpickle_pickle_list_core
 end
 
-definition countable_list [instance] {A : Type} [h : countable A] : countable (list A) :=
+definition countable_list [instance] : countable (list A) :=
 countable.mk
   pickle_list
   unpickle_list