feat(library/init): make sure list, char and string decidable_eq instances are defined in the init folder

library/data/list/basic.lean

@@ -526,20 +526,6 @@ rfl
 end ith
 
 open decidable
-definition has_decidable_eq {A : Type} [H : decidable_eq A] (l₁ : list A) :  ∀ l₂ : list A, decidable (l₁ = l₂) :=
-list.rec_on l₁
-  (λ l₂, list.cases_on l₂
-    (tt rfl)
-    (λ b l₂, ff (λ H, list.no_confusion H)))
-  (λ a l₁ ih l₂, list.cases_on l₂
-    (ff (λ H, list.no_confusion H))
-    (λ b l₂,
-       decidable.cases_on (H a b)
-        (λ Hnab : a ≠ b, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hab Hnab)))
-        (λ Hab : a = b,
-           decidable.cases_on (ih l₂)
-             (λ Hne : l₁ ≠ l₂, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hl₁l₂ Hne)))
-             (λ He  : l₁ = l₂, tt (congr (congr_arg cons Hab) He)))))
 
 /- quasiequal a l l' means that l' is exactly l, with a added
    once somewhere -/
@@ -787,5 +773,4 @@ this (count a l) rfl
 end count
 end list
 
-attribute list.has_decidable_eq [instance]
 attribute list.decidable_mem    [instance]

library/init/char.lean

@@ -15,3 +15,7 @@ definition of_nat [coercion] (n : nat) : char :=
 if H : n < 256 then fin.mk n H else fin.mk 0 dec_trivial
 
 end char
+
+definition char.has_decidable_eq [instance] : decidable_eq char :=
+have decidable_eq (fin 256), from _,
+this

library/init/default.lean

@@ -8,4 +8,4 @@ import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
-import init.monad init.fin init.char init.string
+import init.monad init.fin init.list init.char init.string

library/init/list.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import init.logic
+open decidable list
+
+definition list.has_decidable_eq [instance] {A : Type} [H : decidable_eq A] (l₁ : list A) :  ∀ l₂ : list A, decidable (l₁ = l₂) :=
+list.rec_on l₁
+  (λ l₂, list.cases_on l₂
+    (tt rfl)
+    (λ b l₂, ff (λ H, list.no_confusion H)))
+  (λ a l₁ ih l₂, list.cases_on l₂
+    (ff (λ H, list.no_confusion H))
+    (λ b l₂,
+       decidable.cases_on (H a b)
+        (λ Hnab : a ≠ b, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hab Hnab)))
+        (λ Hab : a = b,
+           decidable.cases_on (ih l₂)
+             (λ Hne : l₁ ≠ l₂, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hl₁l₂ Hne)))
+             (λ He  : l₁ = l₂, tt (congr (congr_arg cons Hab) He)))))

library/init/subtype.lean

@@ -28,12 +28,15 @@ namespace subtype
 
   protected theorem eq : ∀ {a1 a2 : {x | P x}} (H : elt_of a1 = elt_of a2), a1 = a2
   | (tag x1 H1) (tag x2 H2) := tag_eq
+end subtype
 
-  protected definition is_inhabited [instance] {a : A} (H : P a) : inhabited {x | P x} :=
-  inhabited.mk (tag a H)
+open subtype
 
-  protected definition has_decidable_eq [instance] [H : decidable_eq A] : ∀ s₁ s₂ : {x | P x}, decidable (s₁ = s₂)
-  | (tag v₁ p₁) (tag v₂ p₂) :=
+variables {A : Type} {P : A → Prop}
+protected definition subtype.is_inhabited [instance] {a : A} (H : P a) : inhabited {x | P x} :=
+inhabited.mk (tag a H)
+
+protected definition subtype.has_decidable_eq [instance] [H : decidable_eq A] : ∀ s₁ s₂ : {x | P x}, decidable (s₁ = s₂)
+| (tag v₁ p₁) (tag v₂ p₂) :=
   decidable_of_decidable_of_iff (H v₁ v₂)
     (iff.intro tag_eq (λh, subtype.no_confusion h (λa b, a)))
-end subtype