chore(library/init): use 'instance'

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

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

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

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