From 001e06abdc8c1eef03f4ade2ca502f765d97afa3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Sep 2016 13:59:04 -0700
Subject: [PATCH] chore(library/init): use 'instance'

---
 library/init/fin.lean                 |  2 +-
 library/init/meta/expr.lean           |  7 ++++---
 library/init/nat.lean                 | 11 ++++-------
 tests/lean/run/occurs_check_bug1.lean |  2 +-
 4 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/library/init/fin.lean b/library/init/fin.lean
index 673402b683..a8d21a7eb5 100644
--- a/library/init/fin.lean
+++ b/library/init/fin.lean
@@ -24,7 +24,7 @@ open fin
 
 instance (n : nat) : decidable_eq (fin n)
 | ⟨ival, ilt⟩ ⟨jval, jlt⟩ :=
-  match nat.has_decidable_eq ival jval with
+  match nat.decidable_eq ival jval with
   | is_true  h₁ := is_true (eq_of_veq h₁)
   | is_false h₁ := is_false (λ h₂, absurd (veq_of_eq h₂) h₁)
   end
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 673b7d8132..7d626711af 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -24,9 +24,8 @@ inductive expr
 | elet        : name → expr → expr → expr → expr
 | macro       : macro_def → ∀ n : unsigned, (fin (unsigned.to_nat n) → expr) → expr
 
-attribute [instance]
-definition expr.is_inhabited : inhabited expr :=
-inhabited.mk (expr.sort level.zero)
+instance : inhabited expr :=
+⟨expr.sort level.zero⟩
 
 meta_constant expr.mk_macro (d : macro_def) : list expr → expr
 meta_definition expr.mk_var (n : nat) : expr :=
@@ -34,10 +33,12 @@ expr.var (unsigned.of_nat n)
 
 meta_constant expr.has_decidable_eq : decidable_eq expr
 attribute [instance] expr.has_decidable_eq
+
 meta_constant expr.alpha_eqv : expr → expr → bool
 notation a ` =ₐ `:50 b:50 := expr.alpha_eqv a b = bool.tt
 
 meta_constant expr.to_string : expr → string
+
 attribute [instance]
 meta_definition expr.has_to_string : has_to_string expr :=
 has_to_string.mk expr.to_string
diff --git a/library/init/nat.lean b/library/init/nat.lean
index a7eb79f103..6791288fa7 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -115,13 +115,12 @@ namespace nat
   instance : has_mul ℕ :=
   ⟨nat.mul⟩
 
-  attribute [instance, priority nat.prio]
-  protected definition has_decidable_eq : decidable_eq ℕ
+  instance : decidable_eq ℕ
   | 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 has_decidable_eq x y with
+      match decidable_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))
       end
@@ -266,8 +265,7 @@ namespace nat
   theorem lt_of_succ_lt_succ {a b : ℕ} : succ a < succ b → a < b :=
   le_of_succ_le_succ
 
-  attribute [instance, priority nat.prio]
-  protected definition decidable_le : ∀ a b : ℕ, decidable (a ≤ b)
+  instance decidable_le : ∀ a b : ℕ, decidable (a ≤ b)
   | 0     b     := is_true (zero_le b)
   | (a+1) 0     := is_false (not_succ_le_zero a)
   | (a+1) (b+1) :=
@@ -276,8 +274,7 @@ namespace nat
     | is_false h := is_false (λ a, h (le_of_succ_le_succ a))
     end
 
-  attribute [instance, priority nat.prio]
-  protected definition decidable_lt : ∀ a b : ℕ, decidable (a < b) :=
+  instance decidable_lt : ∀ a b : ℕ, decidable (a < b) :=
   λ a b, nat.decidable_le (succ a) b
 
   protected theorem lt_or_ge : ∀ (a b : ℕ), a < b ∨ a ≥ b
diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean
index 82cb5b0311..5479cea8eb 100644
--- a/tests/lean/run/occurs_check_bug1.lean
+++ b/tests/lean/run/occurs_check_bug1.lean
@@ -8,7 +8,7 @@ constant gcd_aux : ℕ × ℕ → ℕ
 
 noncomputable definition gcd (x y : ℕ) : ℕ := gcd_aux (x, y)
 
-theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.has_decidable_eq (snd (x, y)) 0) nat x (gcd y (x mod y)) :=
+theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.decidable_eq (snd (x, y)) 0) nat x (gcd y (x mod y)) :=
 sorry
 
 constant succ_ne_zero (a : nat) : succ a ≠ 0