feat(library/init/core): decidable_eq is a proper class

We need this to take advantage of the new indexing structure we are
going to add to improve performance.

library/init/coe.lean

@@ -155,7 +155,7 @@ instance coe_bool_to_Prop : has_coe bool Prop :=
 ⟨Prop, λ y, y = tt⟩
 
 instance coe_decidable_eq (x : bool) : decidable (coe x) :=
-show decidable (x = tt), from bool.decidable_eq x tt
+show decidable (x = tt), from dec_eq x tt
 
 instance coe_subtype {a : Sort u} {p : a → Prop} : has_coe {x // p x} a :=
 ⟨subtype.val⟩

library/init/core.lean

@@ -298,17 +298,19 @@ class inductive decidable (p : Prop)
 | is_false (h : ¬p) : decidable
 | is_true  (h : p) : decidable
 
-@[reducible]
-def decidable_pred {α : Sort u} (r : α → Prop) :=
+@[reducible] def decidable_pred {α : Sort u} (r : α → Prop) :=
 Π (a : α), decidable (r a)
 
-@[reducible]
-def decidable_rel {α : Sort u} (r : α → α → Prop) :=
+@[reducible] def decidable_rel {α : Sort u} (r : α → α → Prop) :=
 Π (a b : α), decidable (r a b)
 
-@[reducible]
-def decidable_eq (α : Sort u) :=
-decidable_rel (@eq α)
+class decidable_eq (α : Sort u) :=
+{dec_eq : Π a b : α, decidable (a = b)}
+
+export decidable_eq (dec_eq)
+
+instance decidable_of_decidable_eq {α : Sort u} (a b : α) [decidable_eq α] : decidable (a = b) :=
+dec_eq a b
 
 inductive option (α : Type u)
 | none {} : option
@@ -1227,27 +1229,28 @@ theorem bool.ff_ne_tt : ff = tt → false
 def is_dec_eq {α : Sort u} (p : α → α → bool) : Prop   := ∀ ⦃x y : α⦄, p x y = tt → x = y
 def is_dec_refl {α : Sort u} (p : α → α → bool) : Prop := ∀ x, p x x = tt
 
-instance : decidable_eq bool
-| ff ff := is_true rfl
-| ff tt := is_false bool.ff_ne_tt
-| tt ff := is_false (ne.symm bool.ff_ne_tt)
-| tt tt := is_true rfl
+instance : decidable_eq bool :=
+{dec_eq := λ a b, match a, b with
+ | ff, ff := is_true rfl
+ | ff, tt := is_false bool.ff_ne_tt
+ | tt, ff := is_false (ne.symm bool.ff_ne_tt)
+ | tt, tt := is_true rfl}
 
 def decidable_eq_of_bool_pred {α : Sort u} {p : α → α → bool} (h₁ : is_dec_eq p) (h₂ : is_dec_refl p) : decidable_eq α :=
-assume x y : α,
+{dec_eq := λ x y : α,
  if hp : p x y = tt then is_true (h₁ hp)
- else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z _, ¬p z y = tt) _ hxy hp))
+ else is_false (assume hxy : x = y, absurd (h₂ y) (@eq.rec_on _ _ (λ z _, ¬p z y = tt) _ hxy hp))}
 
-theorem decidable_eq_inl_refl {α : Sort u} [h : decidable_eq α] (a : α) : h a a = is_true (eq.refl a) :=
-match (h a a) with
+theorem decidable_eq_inl_refl {α : Sort u} [decidable_eq α] (a : α) : dec_eq a a = is_true (eq.refl a) :=
+match (dec_eq a a) with
 | (is_true e)  := rfl
 | (is_false n) := absurd rfl n
 
-theorem decidable_eq_inr_neg {α : Sort u} [h : decidable_eq α] {a b : α} : Π n : a ≠ b, h a b = is_false n :=
+theorem decidable_eq_inr_neg {α : Sort u} [decidable_eq α] {a b : α} : Π n : a ≠ b, dec_eq a b = is_false n :=
 assume n,
-match (h a b) with
-| (is_true e)   := absurd e n
-| (is_false n₁) := proof_irrel n n₁ ▸ eq.refl (is_false n)
+match dec_eq a b with
+| is_true e   := absurd e n
+| is_false n₁ := proof_irrel n n₁ ▸ eq.refl (is_false n)
 
 /- if-then-else expression theorems -/
 
@@ -1611,10 +1614,10 @@ subtype.eq rfl
 instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : inhabited {x // p x} :=
 ⟨⟨a, h⟩⟩
 
-instance {α : Type u} {p : α → Prop} [decidable_eq α] : decidable_eq {x : α // p x}
-| ⟨a, h₁⟩ ⟨b, h₂⟩ :=
+instance {α : Type u} {p : α → Prop} [decidable_eq α] : decidable_eq {x : α // p x} :=
+{dec_eq := λ ⟨a, h₁⟩ ⟨b, h₂⟩,
   if h : a = b then is_true (subtype.eq h)
-  else is_false (λ h', subtype.no_confusion h' (λ h', absurd h' h))
+  else is_false (λ h', subtype.no_confusion h' (λ h', absurd h' h))}
 end subtype
 
 /- Sum -/
@@ -1630,13 +1633,15 @@ instance sum.inhabited_left [h : inhabited α] : inhabited (α ⊕ β) :=
 instance sum.inhabited_right [h : inhabited β] : inhabited (α ⊕ β) :=
 ⟨sum.inr (default β)⟩
 
-instance {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] : decidable_eq (α ⊕ β)
-| (sum.inl a) (sum.inl b) := if h : a = b then is_true (h ▸ rfl)
-                             else is_false (λ h', sum.no_confusion h' (λ h', absurd h' h))
-| (sum.inr a) (sum.inr b) := if h : a = b then is_true (h ▸ rfl)
-                             else is_false (λ h', sum.no_confusion h' (λ h', absurd h' h))
-| (sum.inr a) (sum.inl b) := is_false (λ h, sum.no_confusion h)
-| (sum.inl a) (sum.inr b) := is_false (λ h, sum.no_confusion h)
+instance {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] : decidable_eq (α ⊕ β) :=
+{dec_eq := λ a b,
+ match a, b with
+ | (sum.inl a), (sum.inl b) := if h : a = b then is_true (h ▸ rfl)
+                               else is_false (λ h', sum.no_confusion h' (λ h', absurd h' h))
+ | (sum.inr a), (sum.inr b) := if h : a = b then is_true (h ▸ rfl)
+                               else is_false (λ h', sum.no_confusion h' (λ h', absurd h' h))
+ | (sum.inr a), (sum.inl b) := is_false (λ h, sum.no_confusion h)
+ | (sum.inl a), (sum.inr b) := is_false (λ h, sum.no_confusion h)}
 end
 
 /- Product -/
@@ -1650,23 +1655,22 @@ theorem prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p
 instance [inhabited α] [inhabited β] : inhabited (prod α β) :=
 ⟨(default α, default β)⟩
 
-instance [h₁ : decidable_eq α] [h₂ : decidable_eq β] : decidable_eq (α × β)
-| (a, b) (a', b') :=
-  match (h₁ a a') with
+instance [decidable_eq α] [decidable_eq β] : decidable_eq (α × β) :=
+{dec_eq := λ ⟨a, b⟩ ⟨a', b'⟩,
+  match (dec_eq a a') with
   | (is_true e₁) :=
-    (match (h₂ b b') with
+    (match (dec_eq b b') with
      | (is_true e₂)  := is_true (eq.rec_on e₁ (eq.rec_on e₂ rfl))
      | (is_false n₂) := is_false (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₂' n₂)))
-  | (is_false n₁) := is_false (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₁' n₁))
+  | (is_false n₁) := is_false (assume h, prod.no_confusion h (λ e₁' e₂', absurd e₁' n₁))}
 
 instance [has_lt α] [has_lt β] : has_lt (α × β) :=
 ⟨λ s t, s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩
 
 instance prod_has_decidable_lt
-         [has_lt α] [has_lt β]
-         [decidable_eq α] [decidable_eq β]
-         [decidable_rel ((<) : α → α → Prop)]
-         [decidable_rel ((<) : β → β → Prop)] : Π s t : α × β, decidable (s < t) :=
+         [has_lt α] [has_lt β] [decidable_eq α] [decidable_eq β]
+         [Π a b : α, decidable (a < b)] [Π a b : β, decidable (a < b)]
+         : Π s t : α × β, decidable (s < t) :=
 λ t s, or.decidable
 
 theorem prod.lt_def [has_lt α] [has_lt β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
@@ -1714,7 +1718,7 @@ instance : inhabited punit :=
 ⟨()⟩
 
 instance : decidable_eq punit :=
-λ a b, is_true (punit_eq a b)
+{dec_eq := λ a b, is_true (punit_eq a b)}
 
 /- Setoid -/
 
@@ -2025,12 +2029,12 @@ eqv_gen.rec_on H
 end
 
 instance {α : Sort u} {s : setoid α} [d : ∀ a b : α, decidable (a ≈ b)] : decidable_eq (quotient s) :=
-λ q₁ q₂ : quotient s,
+{dec_eq := λ q₁ q₂ : quotient s,
   quotient.rec_on_subsingleton₂ q₁ q₂
     (λ a₁ a₂,
       match (d a₁ a₂) with
       | (is_true h₁)  := is_true (quotient.sound h₁)
-      | (is_false h₂) := is_false (λ h, absurd (quotient.exact h) h₂))
+      | (is_false h₂) := is_false (λ h, absurd (quotient.exact h) h₂))}
 
 /- Function extensionality -/
 
@@ -2168,7 +2172,7 @@ noncomputable def decidable_inhabited (a : Prop) : inhabited (decidable a) :=
 local attribute [instance] decidable_inhabited
 
 noncomputable def type_decidable_eq (α : Sort u) : decidable_eq α :=
-λ x y, prop_decidable (x = y)
+{dec_eq := λ x y, prop_decidable (x = y)}
 
 noncomputable def type_decidable (α : Sort u) : psum α (α → false) :=
 match (prop_decidable (nonempty α)) with

library/init/data/char/basic.lean

@@ -66,8 +66,8 @@ lemma vne_of_ne {c d : char} (h : c ≠ d) : c.val ≠ d.val :=
 λ h', absurd (eq_of_veq h') h
 
 instance : decidable_eq char :=
-λ i j, decidable_of_decidable_of_iff
-  (nat.decidable_eq i.val j.val) ⟨char.eq_of_veq, char.veq_of_eq⟩
+{dec_eq := λ i j, decidable_of_decidable_of_iff
+  (dec_eq i.val j.val) ⟨char.eq_of_veq, char.veq_of_eq⟩}
 
 instance : inhabited char :=
 ⟨'A'⟩

library/init/data/fin/basic.lean

@@ -94,5 +94,5 @@ end fin
 open fin
 
 instance (n : nat) : decidable_eq (fin n) :=
-λ i j, decidable_of_decidable_of_iff
-  (nat.decidable_eq i.val j.val) ⟨eq_of_veq, veq_of_eq⟩
+{dec_eq := λ i j, decidable_of_decidable_of_iff
+  (dec_eq i.val j.val) ⟨eq_of_veq, veq_of_eq⟩}

library/init/data/int/basic.lean

@@ -15,15 +15,16 @@ inductive int : Type
 | of_nat : nat → int
 | neg_succ_of_nat : nat → int
 
-instance : decidable_eq int
-| (int.of_nat a) (int.of_nat b) :=
-  if h : a = b then is_true (h ▸ rfl)
-  else is_false (λ h', int.no_confusion h' (λ h', absurd h' h))
-| (int.neg_succ_of_nat a) (int.neg_succ_of_nat b) :=
-  if h : a = b then is_true (h ▸ rfl)
-  else is_false (λ h', int.no_confusion h' (λ h', absurd h' h))
-| (int.of_nat a) (int.neg_succ_of_nat b) := is_false (λ h, int.no_confusion h)
-| (int.neg_succ_of_nat a) (int.of_nat b) := is_false (λ h, int.no_confusion h)
+instance : decidable_eq int :=
+{dec_eq := λ a b, match a, b with
+ | (int.of_nat a), (int.of_nat b) :=
+   if h : a = b then is_true (h ▸ rfl)
+   else is_false (λ h', int.no_confusion h' (λ h', absurd h' h))
+ | (int.neg_succ_of_nat a), (int.neg_succ_of_nat b) :=
+   if h : a = b then is_true (h ▸ rfl)
+   else is_false (λ h', int.no_confusion h' (λ h', absurd h' h))
+ | (int.of_nat a), (int.neg_succ_of_nat b) := is_false (λ h, int.no_confusion h)
+ | (int.neg_succ_of_nat a), (int.of_nat b) := is_false (λ h, int.no_confusion h)}
 
 notation `ℤ` := int
 

library/init/data/list/basic.lean

@@ -16,12 +16,12 @@ variables {α : Type u} {β : Type v} {γ : Type w}
 
 namespace list
 
-protected def has_dec_eq [s : decidable_eq α] : decidable_eq (list α)
+protected def has_dec_eq [decidable_eq α] : Π a b : list α, decidable (a = b)
 | []      []      := is_true rfl
 | (a::as) []      := is_false (λ h, list.no_confusion h)
 | []      (b::bs) := is_false (λ h, list.no_confusion h)
 | (a::as) (b::bs) :=
-  match s a b with
+  match dec_eq a b with
   | is_true hab  :=
     (match has_dec_eq as bs with
      | is_true habs  := is_true (eq.subst hab (eq.subst habs rfl))
@@ -29,7 +29,7 @@ protected def has_dec_eq [s : decidable_eq α] : decidable_eq (list α)
   | is_false nab := is_false (λ h, list.no_confusion h (λ hab _, absurd hab nab))
 
 instance [decidable_eq α] : decidable_eq (list α) :=
-list.has_dec_eq
+{dec_eq := list.has_dec_eq}
 
 protected def append : list α → list α → list α
 | []       l := l
@@ -153,7 +153,8 @@ def find_index (p : α → Prop) [decidable_pred p] : list α → nat
 | []     := 0
 | (a::l) := if p a then 0 else succ (find_index l)
 
-def index_of [decidable_eq α] (a : α) : list α → nat := find_index (eq a)
+def index_of [decidable_eq α] (a : α) (l : list α) : nat :=
+@find_index _ (eq a) (dec_eq a) l
 
 def assoc [decidable_eq α] : list (α × β) → α → option β
 | []         _  := none

library/init/data/nat/basic.lean

@@ -35,7 +35,9 @@ theorem ne_of_beq_eq_ff : ∀ {n m : nat}, beq n m = ff → n ≠ m
   nat.no_confusion h₂ (λ h₂, absurd h₂ this)
 
 instance : decidable_eq nat :=
-λ n m, if h : beq n m = tt then is_true (eq_of_beq_eq_tt h) else is_false (ne_of_beq_eq_ff (eq_ff_of_ne_tt h))
+{dec_eq := λ n m,
+ if h : beq n m = tt then is_true (eq_of_beq_eq_tt h)
+ else is_false (ne_of_beq_eq_ff (eq_ff_of_ne_tt h))}
 
 def ble : nat → nat → bool
 | zero     zero     := tt
@@ -245,11 +247,11 @@ theorem pred_le_pred : ∀ {n m : nat}, n ≤ m → pred n ≤ pred m
 theorem le_of_succ_le_succ {n m : nat} : succ n ≤ succ m → n ≤ m :=
 pred_le_pred
 
-instance decidable_le : ∀ n m : nat, decidable (n ≤ m) :=
-λ n m, bool.decidable_eq _ _
+instance decidable_le (n m : nat) : decidable (n ≤ m) :=
+dec_eq (ble n m) tt
 
-instance decidable_lt : ∀ n m : nat, decidable (n < m) :=
-λ n m, nat.decidable_le (succ n) m
+instance decidable_lt (n m : nat) : decidable (n < m) :=
+nat.decidable_le (succ n) m
 
 protected theorem eq_or_lt_of_le : ∀ {n m: nat}, n ≤ m → n = m ∨ n < m
 | zero     zero     h := or.inl rfl

library/init/data/option/basic.lean

@@ -73,13 +73,14 @@ end option
 instance (α : Type u) : inhabited (option α) :=
 ⟨none⟩
 
-instance {α : Type u} [d : decidable_eq α] : decidable_eq (option α)
-| none      none      := is_true rfl
-| none      (some v₂) := is_false (λ h, option.no_confusion h)
-| (some v₁) none      := is_false (λ h, option.no_confusion h)
-| (some v₁) (some v₂) :=
-  match (d v₁ v₂) with
-  | (is_true e)  := is_true (congr_arg (@some α) e)
-  | (is_false n) := is_false (λ h, option.no_confusion h (λ e, absurd e n))
+instance {α : Type u} [decidable_eq α] : decidable_eq (option α) :=
+{dec_eq := λ a b, match a, b with
+ | none,      none      := is_true rfl
+ | none,      (some v₂) := is_false (λ h, option.no_confusion h)
+ | (some v₁), none      := is_false (λ h, option.no_confusion h)
+ | (some v₁), (some v₂) :=
+   match dec_eq v₁ v₂ with
+   | (is_true e)  := is_true (congr_arg (@some α) e)
+   | (is_false n) := is_false (λ h, option.no_confusion h (λ e, absurd e n))}
 
 instance {α : Type u} [has_lt α] : has_lt (option α) := ⟨option.lt (<)⟩

library/init/data/ordering/basic.lean

@@ -40,7 +40,7 @@ def cmp {α : Type u} [has_lt α] [decidable_rel ((<) : α → α → Prop)] (a
 cmp_using (<) a b
 
 instance : decidable_eq ordering :=
-λ a b,
+{dec_eq := λ a b,
   match a with
   | ordering.lt :=
     (match b with
@@ -56,4 +56,4 @@ instance : decidable_eq ordering :=
     match b with
     | ordering.lt := is_false (λ h, ordering.no_confusion h)
     | ordering.eq := is_false (λ h, ordering.no_confusion h)
-    | ordering.gt := is_true rfl
+    | ordering.gt := is_true rfl}

library/init/data/rbtree/basic.lean

@@ -22,9 +22,9 @@ inductive color
 open color nat
 
 instance color.decidable_eq : decidable_eq color :=
-λ a b, color.cases_on a
+{dec_eq := λ a b, color.cases_on a
   (color.cases_on b (is_true rfl) (is_false (λ h, color.no_confusion h)))
-  (color.cases_on b (is_false (λ h, color.no_confusion h)) (is_true rfl))
+  (color.cases_on b (is_false (λ h, color.no_confusion h)) (is_true rfl))}
 
 def depth (f : nat → nat → nat) : rbnode α → nat
 | leaf               := 0

library/init/data/string/basic.lean

@@ -19,7 +19,9 @@ structure string_imp :=
 def string := string_imp
 
 instance : decidable_eq string :=
-λ ⟨s₁⟩ ⟨s₂⟩, if h : s₁ = s₂ then is_true (congr_arg _ h) else is_false (λ h', string_imp.no_confusion h' (λ h', absurd h' h))
+{dec_eq := λ ⟨s₁⟩ ⟨s₂⟩,
+ if h : s₁ = s₂ then is_true (congr_arg _ h)
+ else is_false (λ h', string_imp.no_confusion h' (λ h', absurd h' h))}
 
 def list.as_string (s : list char) : string :=
 ⟨s⟩

library/init/lean/ir/instances.lean

@@ -28,10 +28,10 @@ theorem id2type_type2id_eq : ∀ (ty : type), id2type (type2id ty) = ty
 | type.float  := rfl  | type.double := rfl  | type.object := rfl
 
 instance type_has_dec_eq : decidable_eq type :=
-λ t₁ t₂,
+{dec_eq := λ t₁ t₂,
  if h : type2id t₁ = type2id t₂
  then is_true (id2type_type2id_eq t₁ ▸ id2type_type2id_eq t₂ ▸ h ▸ rfl)
- else is_false (λ h', absurd rfl (@eq.subst _ (λ t, ¬ type2id t = type2id t₂) _ _ h' h))
+ else is_false (λ h', absurd rfl (@eq.subst _ (λ t, ¬ type2id t = type2id t₂) _ _ h' h))}
 /- END of TEMPORARY HACK for (decidable_eq type) -/
 
 instance : has_coe string fnid :=

library/init/lean/name.lean

@@ -51,17 +51,17 @@ def update_prefix : name → name → name
 | (mk_string p s)  new_p := mk_string new_p s
 | (mk_numeral p s) new_p := mk_numeral new_p s
 
-instance has_decidable_eq : decidable_eq name
+protected def has_dec_eq : Π a b : name, decidable (a = b)
 | anonymous          anonymous          := is_true rfl
 | (mk_string p₁ s₁)  (mk_string p₂ s₂)  :=
   if h₁ : s₁ = s₂ then
-    match has_decidable_eq p₁ p₂ with
+    match has_dec_eq p₁ p₂ with
     | is_true h₂  := is_true $ h₁ ▸ h₂ ▸ rfl
     | is_false h₂ := is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hp h₂
   else is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hs h₁
 | (mk_numeral p₁ n₁) (mk_numeral p₂ n₂) :=
   if h₁ : n₁ = n₂ then
-    match has_decidable_eq p₁ p₂ with
+    match has_dec_eq p₁ p₂ with
     | is_true h₂  := is_true $ h₁ ▸ h₂ ▸ rfl
     | is_false h₂ := is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hp h₂
   else is_false $ λ h, name.no_confusion h $ λ hp hs, absurd hs h₁
@@ -72,6 +72,9 @@ instance has_decidable_eq : decidable_eq name
 | (mk_numeral _ _)   anonymous          := is_false $ λ h, name.no_confusion h
 | (mk_numeral _ _)   (mk_string _ _)    := is_false $ λ h, name.no_confusion h
 
+instance : decidable_eq name :=
+{dec_eq := name.has_dec_eq}
+
 def replace_prefix : name → name → name → name
 | anonymous anonymous new_p := new_p
 | anonymous _         _     := anonymous

library/init/lean/pos.lean

@@ -12,11 +12,12 @@ structure pos :=
 (line   : nat)
 (column : nat)
 
-instance : decidable_eq pos
-| ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ := if h₁ : l₁ = l₂ then
+instance : decidable_eq pos :=
+{dec_eq := λ ⟨l₁, c₁⟩ ⟨l₂, c₂⟩,
+  if h₁ : l₁ = l₂ then
   if h₂ : c₁ = c₂ then is_true (eq.rec_on h₁ (eq.rec_on h₂ rfl))
   else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₂ h₂))
-else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h₁))
+  else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h₁))}
 
 def pos.lt : pos → pos → Prop
 | ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ := (l₁, c₁) < (l₂, c₂)

library/init/meta/name.lean

@@ -30,7 +30,7 @@ protected meta def name.lt (a b : name) : Prop :=
 name.cmp a b = ordering.lt
 
 meta instance : decidable_rel name.lt :=
-λ a b, ordering.decidable_eq _ _
+λ a b, dec_eq (name.cmp a b) ordering.lt
 
 meta instance : has_lt name :=
 ⟨name.lt⟩

library/init/meta/pos.lean

@@ -11,8 +11,9 @@ structure pos :=
 (line   : nat)
 (column : nat)
 
-instance : decidable_eq pos
-| ⟨l₁, c₁⟩ ⟨l₂, c₂⟩ := if h₁ : l₁ = l₂ then
-  if h₂ : c₁ = c₂ then is_true (eq.rec_on h₁ (eq.rec_on h₂ rfl))
-  else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₂ h₂))
-else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h₁))
+instance : decidable_eq pos :=
+{dec_eq := λ ⟨l₁, c₁⟩ ⟨l₂, c₂⟩,
+ if h₁ : l₁ = l₂ then
+ if h₂ : c₁ = c₂ then is_true (eq.rec_on h₁ (eq.rec_on h₂ rfl))
+ else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₂ h₂))
+ else is_false (λ contra, pos.no_confusion contra (λ e₁ e₂, absurd e₁ h₁))}

src/util/nat.h

@@ -25,7 +25,7 @@ public:
     }
     nat(nat const & other):object_ref(other) {}
     nat(nat && other):object_ref(other) {}
-    explicit nat(object * o):object_ref(o) { inc(o); }
+    explicit nat(object * o):object_ref(o) {}
 
     nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
     nat & operator=(nat && other) { object_ref::operator=(other); return *this; }

tests/lean/parsec1.lean

@@ -133,7 +133,7 @@ inductive Expr
 
 open Expr
 
-instance eq_expr : decidable_eq Expr
+def eq_expr : Π a b : Expr, decidable (a = b)
 | (Var x)     (Var y)     := if h : x = y then is_true (h ▸ rfl)
                              else is_false (λ h', Expr.no_confusion h' (λ h', absurd h' h))
 | (Var x)     (Num n)     := is_false (λ h, Expr.no_confusion h)
@@ -151,6 +151,9 @@ instance eq_expr : decidable_eq Expr
                     | is_false h' := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₂ h')))
   | is_false h := is_false (λ he, Expr.no_confusion he (λ h₁ h₂, absurd h₁ h))
 
+instance : decidable_eq Expr :=
+{dec_eq := eq_expr}
+
 def parse_atom (p : parsec' Expr) : parsec' Expr :=
 (Var <$> lexeme var <?> "variable")
 <|>

tests/lean/trust0/basic.lean

@@ -49,15 +49,18 @@ instance : has_sub ℕ :=
 instance : has_mul ℕ :=
 ⟨nat.mul⟩
 
-instance : decidable_eq ℕ
+def has_dec_eq : Π a b : nat, decidable (a = b)
 | zero     zero     := is_true rfl
 | (succ x) zero     := is_false (λ h, nat.no_confusion h)
 | zero     (succ y) := is_false (λ h, nat.no_confusion h)
 | (succ x) (succ y) :=
-    match decidable_eq x y with
+    match has_dec_eq x y with
     | is_true xeqy := is_true (xeqy ▸ eq.refl (succ x))
     | is_false xney := is_false (λ h, nat.no_confusion h (λ xeqy, absurd xeqy xney))
 
+instance : decidable_eq ℕ :=
+{dec_eq := has_dec_eq}
+
 def {u} repeat {α : Type u} (f : ℕ → α → α) : ℕ → α → α
 | 0         a := a
 | (succ n)  a := f n (repeat n a)
@@ -67,7 +70,7 @@ rfl
 
 /- properties of inequality -/
 
-@[refl] protected def le_refl : ∀ a : ℕ, a ≤ a :=
+protected def le_refl : ∀ a : ℕ, a ≤ a :=
 less_than_or_equal.refl
 
 lemma le_succ (n : ℕ) : n ≤ succ n :=