diff --git a/doc/lean/reducible.org b/doc/lean/reducible.org
index 27f623472..428471720 100644
--- a/doc/lean/reducible.org
+++ b/doc/lean/reducible.org
@@ -58,42 +58,28 @@ The following command declares a transparent definition =pr= and mark it as redu
 definition pr1 [reducible] (A : Type) (a b : A) : A := a
 #+END_SRC
 
-The =reducible= mark is saved in the compiled .olean files.  The user
-can temporarily change the =reducible= and =irreducible= marks using
-the following commands. The temporary modification is effective only in the
+The =reducible= attribute is saved in the compiled .olean files.  The user
+can temporarily change the =reducible= and =irreducible= attributes using
+the =attribute= command. The temporary modification is effective only in the
 current file, and is not saved in the produced .olean file.
 
 #+BEGIN_SRC lean
   definition id (A : Type) (a : A) : A := a
   definition pr2 (A : Type) (a b : A) : A := b
   -- mark pr2 as reducible
-  reducible pr2
+  attribute pr2 [reducible]
   -- ...
   -- mark id and pr2 as irreducible
-  irreducible id pr2
+  attribute id [irreducible]
+  attribute pr2 [irreducible]
 #+END_SRC
 
-The annotation =[persistent]= can be used to instruct Lean to make the
+The command =persistent attribute= can be used to instruct Lean to make the
 modification permanent, and save it in the .olean file.
 
 #+BEGIN_SRC lean
   definition pr2 (A : Type) (a b : A) : A := b
   -- Mark pr2 as irreducible.
   -- The modification will affect modules that import this one.
-  irreducible [persistent] pr2
+  persistent attribute pr2 [irreducible]
 #+END_SRC
-
-The reducible and irreducible annotations can be removed using the modifier =[none]=.
-
-#+BEGIN_SRC lean
-  definition pr2 (A : Type) (a b : A) : A := b
-
-  -- temporarily remove any reducible and irreducible annotation from pr2
-  reducible [none] pr2
-
-  -- permanently remove any reducible and irreducible annotation from pr2
-  reducible [persistent] [none] pr2
-#+END_SRC
-
-Finally, the command =irreducible= is syntax sugar for =reducible [off]=.
-The commands =reducible= and =reducible [on]= are equivalent.
diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean
index 9c7274d35..7c991a26d 100644
--- a/hott/algebra/category/basic.hlean
+++ b/hott/algebra/category/basic.hlean
@@ -12,7 +12,7 @@ open precategory morphism is_equiv eq truncation nat sigma sigma.ops
 structure category [class] (ob : Type) extends (precategory ob) :=
   (iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
 
-multiple_instances [persistent] category
+persistent attribute category [multiple-instances]
 
 namespace category
   variables {ob : Type} {C : category ob} {a b : ob}
@@ -20,7 +20,7 @@ namespace category
 
   -- Make iso_of_path_equiv a class instance
   -- TODO: Unsafe class instance?
-  instance [persistent] iso_of_path_equiv
+  persistent attribute iso_of_path_equiv [instance]
 
   definition path_of_iso {a b : ob} : a ≅ b → a = b :=
   iso_of_path⁻¹
diff --git a/hott/algebra/category/set.hlean b/hott/algebra/category/set.hlean
index 9c8299ae3..63fbe4b97 100644
--- a/hott/algebra/category/set.hlean
+++ b/hott/algebra/category/set.hlean
@@ -29,7 +29,7 @@ end precategory
 namespace category
 
   universe variable l
-  instance precategory.set_precategory.{l+1 l}
+  attribute precategory.set_precategory.{l+1 l} [instance]
 
   definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A))
     : (a ≅ b) = (a.1 ≃ b.1) :=
diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index 2157ccca0..b5a869c55 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -490,77 +490,76 @@ end add_comm_group
 
 
 /- bundled structures -/
-
 structure Semigroup :=
 (carrier : Type) (struct : semigroup carrier)
 
-coercion Semigroup.carrier
-instance Semigroup.struct
+persistent attribute Semigroup.carrier [coercion]
+persistent attribute Semigroup.struct [instance]
 
 structure CommSemigroup :=
 (carrier : Type) (struct : comm_semigroup carrier)
 
-coercion CommSemigroup.carrier
-instance CommSemigroup.struct
+persistent attribute CommSemigroup.carrier [coercion]
+persistent attribute CommSemigroup.struct [instance]
 
 structure Monoid :=
 (carrier : Type) (struct : monoid carrier)
 
-coercion Monoid.carrier
-instance Monoid.struct
+persistent attribute Monoid.carrier [coercion]
+persistent attribute Monoid.struct [instance]
 
 structure CommMonoid :=
 (carrier : Type) (struct : comm_monoid carrier)
 
-coercion CommMonoid.carrier
-instance CommMonoid.struct
+persistent attribute CommMonoid.carrier [coercion]
+persistent attribute CommMonoid.struct [instance]
 
 structure Group :=
 (carrier : Type) (struct : group carrier)
 
-coercion Group.carrier
-instance Group.struct
+persistent attribute Group.carrier [coercion]
+persistent attribute Group.struct [instance]
 
 structure CommGroup :=
 (carrier : Type) (struct : comm_group carrier)
 
-coercion CommGroup.carrier
-instance CommGroup.struct
+persistent attribute CommGroup.carrier [coercion]
+persistent attribute CommGroup.struct [instance]
 
 structure AddSemigroup :=
 (carrier : Type) (struct : add_semigroup carrier)
 
-coercion AddSemigroup.carrier
-instance AddSemigroup.struct
+persistent attribute AddSemigroup.carrier [coercion]
+persistent attribute AddSemigroup.struct [instance]
 
 structure AddCommSemigroup :=
 (carrier : Type) (struct : add_comm_semigroup carrier)
 
-coercion AddCommSemigroup.carrier
-instance AddCommSemigroup.struct
+persistent attribute AddCommSemigroup.carrier [coercion]
+persistent attribute AddCommSemigroup.struct [instance]
 
 structure AddMonoid :=
 (carrier : Type) (struct : add_monoid carrier)
 
-coercion AddMonoid.carrier
-instance AddMonoid.struct
+persistent attribute AddMonoid.carrier [coercion]
+persistent attribute AddMonoid.struct [instance]
 
 structure AddCommMonoid :=
 (carrier : Type) (struct : add_comm_monoid carrier)
 
-coercion AddCommMonoid.carrier
-instance AddCommMonoid.struct
+persistent attribute AddCommMonoid.carrier [coercion]
+persistent attribute AddCommMonoid.struct [instance]
 
 structure AddGroup :=
 (carrier : Type) (struct : add_group carrier)
 
-coercion AddGroup.carrier
-instance AddGroup.struct
+persistent attribute AddGroup.carrier [coercion]
+persistent attribute AddGroup.struct [instance]
 
 structure AddCommGroup :=
 (carrier : Type) (struct : add_comm_group carrier)
 
-coercion AddCommGroup.carrier
-instance AddCommGroup.struct
+persistent attribute AddCommGroup.carrier [coercion]
+persistent attribute AddCommGroup.struct [instance]
 
 end path_algebra
diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean
index bd00eec79..a9f6270da 100644
--- a/hott/algebra/groupoid.hlean
+++ b/hott/algebra/groupoid.hlean
@@ -14,7 +14,7 @@ structure groupoid [class] (ob : Type) extends precategory ob :=
 
 namespace groupoid
 
-instance [persistent] all_iso
+persistent attribute all_iso [instance]
 
 --set_option pp.universes true
 --set_option pp.implicit true
diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean
index 28eb10eda..252769153 100644
--- a/hott/algebra/precategory/basic.hlean
+++ b/hott/algebra/precategory/basic.hlean
@@ -14,13 +14,13 @@ structure precategory [class] (ob : Type) : Type :=
   (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
   (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
 
-multiple_instances [persistent] precategory
+persistent attribute precategory [multiple-instances]
 
 namespace precategory
   variables {ob : Type} [C : precategory ob]
   variables {a b c d : ob}
   include C
-  instance [persistent] homH
+  persistent attribute homH [instance]
 
   definition compose := comp
 
diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean
index 0fd06385e..8d915e95a 100644
--- a/hott/algebra/precategory/constructions.hlean
+++ b/hott/algebra/precategory/constructions.hlean
@@ -110,7 +110,7 @@ namespace precategory
     infixr `×c`:30 := product.Prod_precategory
     --instance [persistent] type_category category_one
     --                      category_two product.prod_category
-    instance [persistent] product.prod_precategory
+    persistent attribute product.prod_precategory [instance]
 
   end ops
 
diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean
index 66843f7c5..5b1fc5b3c 100644
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@@ -19,8 +19,8 @@ infixl `⇒`:25 := functor
 namespace functor
   variables {C D E : Precategory}
 
-  coercion [persistent] obF
-  coercion [persistent] homF
+  persistent attribute obF [coercion]
+  persistent attribute homF [coercion]
 
   -- "functor C D" is equivalent to a certain sigma type
   set_option unifier.max_steps 38500
@@ -156,7 +156,7 @@ namespace precategory
   namespace ops
 
     notation `PreCat`:max := Precat_of_strict_cats
-    instance [persistent] precat_of_strict_precats
+    persistent attribute precat_of_strict_precats [instance]
 
   end ops
 
diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean
index bc7b16b57..3e21c1074 100644
--- a/hott/algebra/precategory/morphism.hlean
+++ b/hott/algebra/precategory/morphism.hlean
@@ -16,7 +16,7 @@ namespace morphism
   inductive is_iso        [class] (f : a ⟶ b) : Type
   := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
-  multiple_instances [persistent] is_iso
+  persistent attribute is_iso [multiple-instances]
 
   definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
   is_section.rec (λg h, g) H
@@ -133,7 +133,7 @@ namespace morphism
   namespace isomorphic
 
     -- openrelation
-    instance [persistent] is_iso
+    persistent attribute is_iso [instance]
 
     definition refl (a : ob) : a ≅ a :=
     mk id
diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean
index aca3568be..b3d5b4ff8 100644
--- a/hott/init/axioms/funext_varieties.hlean
+++ b/hott/init/axioms/funext_varieties.hlean
@@ -85,7 +85,7 @@ context
     @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f idhtpy) (sigma.mk g h)
       (@path_contr _ contr_basedhtpy _ _) d
 
-  reducible htpy_ind
+  attribute htpy_ind [reducible]
   definition htpy_ind_beta : htpy_ind f idhtpy = d :=
     (@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp
 
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 758ccbc35..048a2d09c 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -212,7 +212,7 @@ end is_equiv
 
 namespace equiv
 
-  instance [persistent] to_is_equiv
+  persistent attribute to_is_equiv [instance]
 
   infix `≃`:25 := equiv
 
diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean
index 0ccd2b3f6..aaff2c60e 100644
--- a/hott/init/hedberg.hlean
+++ b/hott/init/hedberg.hlean
@@ -43,4 +43,4 @@ context
    ... = q                      : aux)
 end
 
-instance [persistent] is_hset_of_decidable_eq
+persistent attribute is_hset_of_decidable_eq [instance]
diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index 526cd7b2d..7fd2a6d89 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -296,7 +296,7 @@ namespace nat
 
   notation a * b := mul a b
 
-  reducible sub
+  attribute sub [reducible]
   definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
   rec_on b
     rfl
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index a9882173a..c6ef3f9ea 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -188,7 +188,7 @@ namespace truncation
 
   structure trunctype (n : trunc_index) :=
   (trunctype_type : Type) (is_trunc_trunctype_type : is_trunc n trunctype_type)
-  coercion trunctype.trunctype_type
+  attribute trunctype.trunctype_type [coercion]
 
   notation n `-Type` := trunctype n
   notation `hprop` := -1-Type
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index b568d194c..ddc02fce6 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -142,7 +142,7 @@ namespace sigma
     apply dpair_eq_dpair_pp_pp
   end
 
-  reducible dpair_eq_dpair
+  attribute dpair_eq_dpair [reducible]
   definition dpair_eq_dpair_p1_1p (p : a = a') (q : p ▹ b = b') :
       dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
   begin
@@ -285,7 +285,8 @@ namespace sigma
   equiv.mk (functor f g) !is_equiv_functor
 
   context --remove
-  irreducible inv function.compose --remove
+  attribute inv [irreducible]
+  attribute function.compose [irreducible] --remove
   definition equiv_functor (Hf : A ≃ A') (Hg : Π a, B a ≃ B' (to_fun Hf a)) :
       (Σa, B a) ≃ (Σa', B' a') :=
   equiv_functor_of_is_equiv (to_fun Hf) (λ a, to_fun (Hg a))
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index e4818cafb..17ea1e45d 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -19,7 +19,7 @@ structure category [class] (ob : Type) : Type :=
   (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
   (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
 
-multiple_instances [persistent] category
+persistent attribute category [multiple-instances]
 
 namespace category
   variables {ob : Type} [C : category ob]
diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
index 36c98aa85..88b007ff5 100644
--- a/library/algebra/category/constructions.lean
+++ b/library/algebra/category/constructions.lean
@@ -77,10 +77,10 @@ namespace category
      (λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _)
      (λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
      (λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
-  reducible discrete_category
+  attribute discrete_category [reducible]
   definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
     context
-    instance discrete_category
+    attribute discrete_category [instance]
     include H
     theorem dicrete_category.endomorphism {a b : A} (f : a ⟶ b) : a = b :=
     decidable.rec_on (H a b) (λh f, h) (λh f, empty.rec _ f) f
@@ -125,8 +125,10 @@ namespace category
     notation 2 := Category_two
     postfix `ᵒᵖ`:max := opposite.Opposite
     infixr `×c`:30 := product.Prod_category
-    instance [persistent] type_category category_one
-                          category_two product.prod_category
+    persistent attribute type_category [instance]
+    persistent attribute category_one [instance]
+    persistent attribute category_two [instance]
+    persistent attribute product.prod_category [instance]
   end ops
 
   open ops
@@ -226,7 +228,7 @@ namespace category
 
   definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c)
   open category.ops
-  instance [persistent] slice_category
+  persistent attribute slice_category [instance]
   variables {D : Category}
   definition forgetful (x : D) : (Slice_category D x) ⇒ D :=
   functor.mk (λ a, to_ob a)
diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean
index 7257b3ffb..0feb78a61 100644
--- a/library/algebra/category/functor.lean
+++ b/library/algebra/category/functor.lean
@@ -21,9 +21,10 @@ structure functor (C D : Category) : Type :=
 infixl `⇒`:25 := functor
 
 namespace functor
-  coercion [persistent] object
-  coercion [persistent] morphism
-  irreducible [persistent] respect_id respect_comp
+  persistent attribute object [coercion]
+  persistent attribute morphism [coercion]
+  persistent attribute respect_id [irreducible]
+  persistent attribute respect_comp [irreducible]
 
   variables {A B C D : Category}
 
@@ -70,7 +71,7 @@ namespace category
 
   namespace ops
     notation `Cat`:max := Category_of_categories
-    instance [persistent] category_of_categories
+    persistent attribute category_of_categories [instance]
   end ops
 end category
 
diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index bb71351f4..f90cc4be0 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -20,7 +20,7 @@ namespace morphism
   inductive is_iso        [class] (f : a ⟶ b) : Type
   := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
 
-  multiple_instances [persistent] is_iso
+  persistent attribute is_iso [multiple-instances]
 
   definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
   is_section.rec (λg h, g) H
@@ -131,7 +131,7 @@ namespace morphism
 
   namespace isomorphic
   open relation
-  instance [persistent] is_iso
+  persistent attribute is_iso [instance]
 
   theorem refl  (a     : ob)                            : a ≅ a := mk id
   theorem symm  ⦃a b   : ob⦄ (H  : a ≅ b)              : b ≅ a := mk (inverse (iso H))
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 1360b1b31..c47998962 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -489,73 +489,73 @@ end add_comm_group
 structure Semigroup :=
 (carrier : Type) (struct : semigroup carrier)
 
-coercion Semigroup.carrier
-instance Semigroup.struct
+persistent attribute Semigroup.carrier [coercion]
+persistent attribute Semigroup.struct [instance]
 
 structure CommSemigroup :=
 (carrier : Type) (struct : comm_semigroup carrier)
 
-coercion CommSemigroup.carrier
-instance CommSemigroup.struct
+persistent attribute CommSemigroup.carrier [coercion]
+persistent attribute CommSemigroup.struct [instance]
 
 structure Monoid :=
 (carrier : Type) (struct : monoid carrier)
 
-coercion Monoid.carrier
-instance Monoid.struct
+persistent attribute Monoid.carrier [coercion]
+persistent attribute Monoid.struct [instance]
 
 structure CommMonoid :=
 (carrier : Type) (struct : comm_monoid carrier)
 
-coercion CommMonoid.carrier
-instance CommMonoid.struct
+persistent attribute CommMonoid.carrier [coercion]
+persistent attribute CommMonoid.struct [instance]
 
 structure Group :=
 (carrier : Type) (struct : group carrier)
 
-coercion Group.carrier
-instance Group.struct
+persistent attribute Group.carrier [coercion]
+persistent attribute Group.struct [instance]
 
 structure CommGroup :=
 (carrier : Type) (struct : comm_group carrier)
 
-coercion CommGroup.carrier
-instance CommGroup.struct
+persistent attribute CommGroup.carrier [coercion]
+persistent attribute CommGroup.struct [instance]
 
 structure AddSemigroup :=
 (carrier : Type) (struct : add_semigroup carrier)
 
-coercion AddSemigroup.carrier
-instance AddSemigroup.struct
+persistent attribute AddSemigroup.carrier [coercion]
+persistent attribute AddSemigroup.struct [instance]
 
 structure AddCommSemigroup :=
 (carrier : Type) (struct : add_comm_semigroup carrier)
 
-coercion AddCommSemigroup.carrier
-instance AddCommSemigroup.struct
+persistent attribute AddCommSemigroup.carrier [coercion]
+persistent attribute AddCommSemigroup.struct [instance]
 
 structure AddMonoid :=
 (carrier : Type) (struct : add_monoid carrier)
 
-coercion AddMonoid.carrier
-instance AddMonoid.struct
+persistent attribute AddMonoid.carrier [coercion]
+persistent attribute AddMonoid.struct [instance]
 
 structure AddCommMonoid :=
 (carrier : Type) (struct : add_comm_monoid carrier)
 
-coercion AddCommMonoid.carrier
-instance AddCommMonoid.struct
+persistent attribute AddCommMonoid.carrier [coercion]
+persistent attribute AddCommMonoid.struct [instance]
 
 structure AddGroup :=
 (carrier : Type) (struct : add_group carrier)
 
-coercion AddGroup.carrier
-instance AddGroup.struct
+persistent attribute AddGroup.carrier [coercion]
+persistent attribute AddGroup.struct [instance]
 
 structure AddCommGroup :=
 (carrier : Type) (struct : add_comm_group carrier)
 
-coercion AddCommGroup.carrier
-instance AddCommGroup.struct
+persistent attribute AddCommGroup.carrier [coercion]
+persistent attribute AddCommGroup.struct [instance]
 
 end algebra
diff --git a/library/data/bool.lean b/library/data/bool.lean
index cd5dfda84..36f1b16e7 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -10,7 +10,8 @@ import logic.eq
 open eq eq.ops decidable
 
 namespace bool
-  reducible bor band rec_on
+  attribute bor [reducible]
+  attribute band [reducible]
 
   theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
   cases_on b (or.inl rfl) (or.inr rfl)
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 392ee518b..1a88a63aa 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -42,7 +42,7 @@ inductive int : Type :=
   neg_succ_of_nat : nat → int
 
 notation `ℤ` := int
-coercion [persistent] int.of_nat
+persistent attribute int.of_nat [coercion]
 definition int.of_num [coercion] [reducible] (n : num) : ℤ := int.of_nat (nat.of_num n)
 
 namespace int
@@ -128,7 +128,7 @@ calc
     ... = of_nat (m - n) : rfl
 
 context
-reducible sub_nat_nat
+attribute sub_nat_nat [reducible]
 theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) :
   sub_nat_nat m n = neg_succ_of_nat (pred (n - m)) :=
 have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_lt H))⁻¹,
@@ -282,7 +282,8 @@ calc
     ... = b : abstr_repr
 
 context
-reducible abstr dist
+attribute abstr [reducible]
+attribute dist [reducible]
 theorem nat_abs_abstr (p : ℕ × ℕ) : nat_abs (abstr p) = dist (pr1 p) (pr2 p) :=
 let m := pr1 p, n := pr2 p in
 or.elim (@le_or_gt n m)
@@ -463,7 +464,7 @@ have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b),
 H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3
 
 context
-reducible nat_abs
+attribute nat_abs [reducible]
 theorem mul_nat_abs (a b : ℤ) : nat_abs (a * b) = #nat (nat_abs a) * (nat_abs b) :=
 cases_on a
   (take m,
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 95a11484b..3723e74cc 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -197,7 +197,8 @@ induction_on s
 theorem mem_concat (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t :=
 iff.intro mem_concat_imp_or mem_or_imp_concat
 
-reducible mem append
+attribute mem [reducible]
+attribute append [reducible]
 theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) :=
 induction_on l
   (take H : x ∈ nil, false.elim (iff.elim_left !mem_nil H))
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 538f451a1..8f8d88be0 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -333,7 +333,7 @@ private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure p
 private definition pair_nat.lt.wf : well_founded pair_nat.lt :=
 intro_k (measure.wf pr₂) 20  -- we use intro_k to be able to execute gcd efficiently in the kernel
 
-instance pair_nat.lt.wf      -- instance will not be saved in .olean
+attribute pair_nat.lt.wf [instance]      -- instance will not be saved in .olean
 infixl [local] `≺`:50 := pair_nat.lt
 
 private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=
diff --git a/library/init/nat.lean b/library/init/nat.lean
index b71813229..683f3353f 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -289,7 +289,7 @@ namespace nat
   notation a * b := mul a b
 
   section
-  reducible sub
+  attribute sub [reducible]
   definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
   induction_on b
     rfl
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 14fd2a43b..da62b89f2 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -8,15 +8,16 @@
 (require 'rx)
 
 (defconst lean-keywords
-  '("import" "prelude" "reducible" "irreducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
+  '("import" "prelude" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "example"
     "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
-    "using" "namespace" "instance" "class" "multiple_instances" "section" "fields" "find_decl"
-    "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")
+    "using" "namespace" "section" "fields" "find_decl"
+    "attribute" "persistent" "set_option" "add_rewrite" "extends" "include" "omit" "classes"
+    "instances" "coercions" "raw")
   "lean keywords")
 
 (defconst lean-syntax-table
@@ -116,7 +117,7 @@
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
      (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
-               "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[wf\]" "\[whnf\]"
+               "\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]"
                "\[decls\]" "\[strict\]" "\[local\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
       . 'font-lock-doc-face)
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index af0a33b0d..db3487f79 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -3,7 +3,7 @@ token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp
 parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
-begin_end_ext.cpp class.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
+begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
 coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp
 init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index bf5c50261..9e5ae69ee 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -35,7 +35,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/find_cmd.h"
 #include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/decl_cmds.h"
-#include "frontends/lean/class.h"
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parse_table.h"
@@ -536,72 +535,6 @@ environment open_export_cmd(parser & p, bool open) {
 environment open_cmd(parser & p) { return open_export_cmd(p, true); }
 environment export_cmd(parser & p) { return open_export_cmd(p, false); }
 
-environment coercion_cmd(parser & p) {
-    if (in_context_or_parametric_section(p))
-        throw parser_error("invalid 'coercion' command, coercions cannot be defined in contexts or "
-                           "sections containing parameters", p.pos());
-    bool persistent = false;
-    parse_persistent(p, persistent);
-    name f   = p.check_constant_next("invalid 'coercion' command, constant expected");
-    if (p.curr_is_token(get_colon_tk())) {
-        p.next();
-        name C = p.check_constant_next("invalid 'coercion' command, constant expected");
-        return add_coercion(p.env(), f, C, p.ios(), persistent);
-    } else {
-        return add_coercion(p.env(), f, p.ios(), persistent);
-    }
-}
-
-static void parse_reducible_modifiers(parser & p, reducible_status & status, bool & persistent) {
-    while (true) {
-        if (parse_persistent(p, persistent)) {
-        } else if (p.curr_is_token_or_id(get_on_tk())) {
-            p.next();
-            status = reducible_status::On;
-        } else if (p.curr_is_token_or_id(get_off_tk())) {
-            p.next();
-            status = reducible_status::Off;
-        } else if (p.curr_is_token_or_id(get_none_tk())) {
-            p.next();
-            status = reducible_status::None;
-        } else {
-            break;
-        }
-    }
-}
-
-environment reducible_cmd(parser & p) {
-    environment env         = p.env();
-    reducible_status status = reducible_status::On;
-    bool persistent         = false;
-    parse_reducible_modifiers(p, status, persistent);
-    bool found = false;
-    while (p.curr_is_identifier()) {
-        name c = p.check_constant_next("invalid 'reducible' command, constant expected");
-        found   = true;
-        env = set_reducible(env, c, status, persistent);
-    }
-    if (!found)
-        throw exception("invalid empty 'reducible' command");
-    return env;
-}
-
-environment irreducible_cmd(parser & p) {
-    environment env         = p.env();
-    reducible_status status = reducible_status::Off;
-    bool persistent         = false;
-    parse_persistent(p, persistent);
-    bool found = false;
-    while (p.curr_is_identifier()) {
-        name c = p.check_constant_next("invalid 'irreducible' command, constant expected");
-        found   = true;
-        env = set_reducible(env, c, status, persistent);
-    }
-    if (!found)
-        throw exception("invalid empty 'irreducible' command");
-    return env;
-}
-
 environment erase_cache_cmd(parser & p) {
     name n = p.check_id_next("invalid #erase_cache command, identifier expected");
     p.erase_cached_definition(n);
@@ -656,9 +589,6 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("end",           "close the current namespace/section", end_scoped_cmd));
     add_cmd(r, cmd_info("check",         "type check given expression, and display its type", check_cmd));
     add_cmd(r, cmd_info("eval",          "evaluate given expression", eval_cmd));
-    add_cmd(r, cmd_info("coercion",      "add a new coercion", coercion_cmd));
-    add_cmd(r, cmd_info("reducible",     "mark definitions as reducible/irreducible for automation", reducible_cmd));
-    add_cmd(r, cmd_info("irreducible",   "mark definitions as irreducible for automation", irreducible_cmd));
     add_cmd(r, cmd_info("find_decl",     "find definitions and/or theorems", find_cmd));
     add_cmd(r, cmd_info("#erase_cache",  "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#projections",  "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
@@ -670,7 +600,6 @@ void init_cmd_table(cmd_table & r) {
     register_notation_cmds(r);
     register_calc_cmds(r);
     register_begin_end_cmds(r);
-    register_class_cmds(r);
     register_tactic_hint_cmd(r);
 }
 
diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp
deleted file mode 100644
index 7124a9c36..000000000
--- a/src/frontends/lean/class.cpp
+++ /dev/null
@@ -1,92 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "library/num.h"
-#include "library/normalize.h"
-#include "library/class.h"
-#include "frontends/lean/parser.h"
-#include "frontends/lean/util.h"
-#include "frontends/lean/tokens.h"
-
-namespace lean {
-optional<unsigned> parse_instance_priority(parser & p) {
-    if (p.curr_is_token(get_priority_tk())) {
-        p.next();
-        auto pos = p.pos();
-        environment env = open_priority_aliases(open_num_notation(p.env()));
-        parser::local_scope scope(p, env);
-        expr val = p.parse_expr();
-        val = normalize(p.env(), val);
-        if (optional<mpz> mpz_val = to_num(val)) {
-            if (!mpz_val->is_unsigned_int())
-                throw parser_error("invalid 'priority', argument does not fit in a machine integer", pos);
-            p.check_token_next(get_rbracket_tk(), "invalid 'priority', ']' expected");
-            return optional<unsigned>(mpz_val->get_unsigned_int());
-        } else {
-            throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos);
-        }
-    } else {
-        return optional<unsigned>();
-    }
-}
-
-environment add_instance_cmd(parser & p) {
-    bool found = false;
-    bool persistent = false;
-    parse_persistent(p, persistent);
-    optional<unsigned> priority = parse_instance_priority(p);
-    environment env = p.env();
-    while (p.curr_is_identifier()) {
-        found    = true;
-        name c   = p.check_constant_next("invalid 'class instance' declaration, constant expected");
-        if (priority)
-            env = add_instance(env, c, *priority, persistent);
-        else
-            env = add_instance(env, c, persistent);
-    }
-    if (!found)
-        throw parser_error("invalid 'class instance' declaration, at least one identifier expected", p.pos());
-    return env;
-}
-
-
-environment add_class_cmd(parser & p) {
-    bool found = false;
-    environment env = p.env();
-    bool persistent = false;
-    parse_persistent(p, persistent);
-    while (p.curr_is_identifier()) {
-        found    = true;
-        name c   = p.check_constant_next("invalid 'class' declaration, constant expected");
-        env = add_class(env, c, persistent);
-    }
-    if (!found)
-        throw parser_error("invalid 'class' declaration, at least one identifier expected", p.pos());
-    return env;
-}
-
-environment multiple_instances_cmd(parser & p) {
-    bool found = false;
-    environment env = p.env();
-    bool persistent = false;
-    parse_persistent(p, persistent);
-    while (p.curr_is_identifier()) {
-        found    = true;
-        name c   = p.check_constant_next("invalid 'multiple_instances' command, constant expected");
-        env = mark_multiple_instances(env, c, persistent);
-    }
-    if (!found)
-        throw parser_error("invalid 'multiple_instances' command, at least one identifier expected", p.pos());
-    return env;
-}
-
-void register_class_cmds(cmd_table & r) {
-    add_cmd(r, cmd_info("instance",           "add a new instance", add_instance_cmd));
-    add_cmd(r, cmd_info("class",              "add a new class", add_class_cmd));
-    add_cmd(r, cmd_info("multiple_instances", "mark that Lean must explore multiple instances of the given class", multiple_instances_cmd));
-}
-}
diff --git a/src/frontends/lean/class.h b/src/frontends/lean/class.h
deleted file mode 100644
index 7c4ba6184..000000000
--- a/src/frontends/lean/class.h
+++ /dev/null
@@ -1,17 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/name.h"
-#include "util/list.h"
-#include "kernel/environment.h"
-#include "frontends/lean/cmd_table.h"
-
-namespace lean {
-/** \brief Parse priority for an class instance */
-optional<unsigned> parse_instance_priority(parser & p);
-void register_class_cmds(cmd_table & r);
-}
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 6ef4a1216..40722e6a4 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -12,7 +12,9 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
+#include "library/num.h"
 #include "library/private.h"
+#include "library/normalize.h"
 #include "library/protected.h"
 #include "library/placeholder.h"
 #include "library/locals.h"
@@ -23,7 +25,6 @@ Author: Leonardo de Moura
 #include "library/unfold_macros.h"
 #include "library/definitional/equations.h"
 #include "frontends/lean/parser.h"
-#include "frontends/lean/class.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
 
@@ -269,15 +270,45 @@ static environment constants_cmd(parser & p) {
     return variables_cmd_core(p, variable_kind::Constant);
 }
 
-struct decl_modifiers {
+struct decl_attributes {
+    bool               m_def_only; // if true only definition attributes are allowed
     bool               m_is_instance;
     bool               m_is_coercion;
     bool               m_is_reducible;
+    bool               m_is_irreducible;
+    bool               m_is_class;
+    bool               m_has_multiple_instances;
     optional<unsigned> m_priority;
-    decl_modifiers():m_priority() {
-        m_is_instance  = false;
-        m_is_coercion  = false;
-        m_is_reducible = false;
+
+    decl_attributes(bool def_only = true):m_priority() {
+        m_def_only               = def_only;
+        m_is_instance            = false;
+        m_is_coercion            = false;
+        m_is_reducible           = false;
+        m_is_irreducible         = false;
+        m_is_class               = false;
+        m_has_multiple_instances = false;
+    }
+
+    optional<unsigned> parse_instance_priority(parser & p) {
+        if (p.curr_is_token(get_priority_tk())) {
+            p.next();
+            auto pos = p.pos();
+            environment env = open_priority_aliases(open_num_notation(p.env()));
+            parser::local_scope scope(p, env);
+            expr val = p.parse_expr();
+            val = normalize(p.env(), val);
+            if (optional<mpz> mpz_val = to_num(val)) {
+                if (!mpz_val->is_unsigned_int())
+                    throw parser_error("invalid 'priority', argument does not fit in a machine integer", pos);
+                p.check_token_next(get_rbracket_tk(), "invalid 'priority', ']' expected");
+                return optional<unsigned>(mpz_val->get_unsigned_int());
+            } else {
+                throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos);
+            }
+        } else {
+            return optional<unsigned>();
+        }
     }
 
     void parse(parser & p) {
@@ -290,20 +321,61 @@ struct decl_modifiers {
                 auto pos = p.pos();
                 p.next();
                 if (in_context(p.env()))
-                    throw parser_error("invalid '[coercion]' modifier, coercions cannot be defined in contexts", pos);
+                    throw parser_error("invalid '[coercion]' attribute, coercions cannot be defined in contexts", pos);
                 m_is_coercion = true;
             } else if (p.curr_is_token(get_reducible_tk())) {
+                if (m_is_irreducible)
+                    throw parser_error("invalid '[reducible]' attribute, '[irreducible]' was already provided", pos);
                 m_is_reducible = true;
                 p.next();
+            } else if (p.curr_is_token(get_irreducible_tk())) {
+                if (m_is_reducible)
+                    throw parser_error("invalid '[irreducible]' attribute, '[reducible]' was already provided", pos);
+                m_is_irreducible = true;
+                p.next();
+            } else if (p.curr_is_token(get_class_tk())) {
+                if (m_def_only)
+                    throw parser_error("invalid '[class]' attribute, definitions cannot be marked as classes", pos);
+                m_is_class = true;
+                p.next();
+            } else if (p.curr_is_token(get_multiple_instances_tk())) {
+                if (m_def_only)
+                    throw parser_error("invalid '[multiple-instances]' attribute, only classes can have this attribute", pos);
+                m_has_multiple_instances = true;
+                p.next();
             } else if (auto it = parse_instance_priority(p)) {
                 m_priority = *it;
                 if (!m_is_instance)
-                    throw parser_error("invalid '[priority]' occurrence, declaration must be marked as an '[instance]'", pos);
+                    throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]'", pos);
             } else {
                 break;
             }
         }
     }
+
+    environment apply(environment env, io_state const & ios, name const & d, bool persistent) {
+        if (m_is_instance) {
+            if (m_priority) {
+                #if defined(__GNUC__) && !defined(__CLANG__)
+                #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
+                #endif
+                env = add_instance(env, d, *m_priority, persistent);
+            } else {
+                env = add_instance(env, d, persistent);
+            }
+        }
+        if (m_is_coercion)
+            env = add_coercion(env, d, ios, persistent);
+        if (m_is_reducible)
+            env = set_reducible(env, d, reducible_status::On, persistent);
+        if (m_is_irreducible)
+            env = set_reducible(env, d, reducible_status::Off, persistent);
+        if (m_is_class)
+            env = add_class(env, d, persistent);
+        if (m_has_multiple_instances)
+            env = mark_multiple_instances(env, d, persistent);
+        return env;
+    }
 };
 
 static void check_end_of_theorem(parser const & p) {
@@ -519,7 +591,7 @@ class definition_cmd_fn {
     pos_info          m_pos;
 
     name              m_name;
-    decl_modifiers    m_modifiers;
+    decl_attributes   m_attributes;
     name              m_real_name; // real name for this declaration
     buffer<name>      m_ls_buffer;
     buffer<name>      m_aux_decls; // user provided names for aux_decls
@@ -550,7 +622,7 @@ class definition_cmd_fn {
         parse_univ_params(m_p, m_ls_buffer);
 
         // Parse modifiers
-        m_modifiers.parse(m_p);
+        m_attributes.parse(m_p);
 
         if (m_p.curr_is_token(get_assign_tk())) {
             auto pos = m_p.pos();
@@ -702,25 +774,12 @@ class definition_cmd_fn {
             // TODO(Leo): register aux_decls
             if (!m_is_private)
                 m_p.add_decl_index(real_n, m_pos, m_p.get_cmd_token(), type);
-            if (n != real_n)
-                m_env = add_expr_alias_rec(m_env, n, real_n);
-            if (m_modifiers.m_is_instance) {
-                bool persistent = true;
-                if (m_modifiers.m_priority) {
-                    #if defined(__GNUC__) && !defined(__CLANG__)
-                    #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
-                    #endif
-                    m_env = add_instance(m_env, real_n, *m_modifiers.m_priority, persistent);
-                } else {
-                    m_env = add_instance(m_env, real_n, persistent);
-                }
-            }
-            if (m_modifiers.m_is_coercion)
-                m_env = add_coercion(m_env, real_n, m_p.ios());
             if (m_is_protected)
                 m_env = add_protected(m_env, real_n);
-            if (m_modifiers.m_is_reducible)
-                m_env = set_reducible(m_env, real_n, reducible_status::On);
+            if (n != real_n)
+                m_env = add_expr_alias_rec(m_env, n, real_n);
+            bool persistent = true;
+            m_env = m_attributes.apply(m_env, m_p.ios(), real_n, persistent);
         }
     }
 
@@ -947,6 +1006,23 @@ static environment omit_cmd(parser & p) {
     return include_cmd_core(p, false);
 }
 
+static environment attribute_cmd_core(parser & p, bool persistent) {
+    name d          = p.check_constant_next("invalid 'attribute' command, constant expected");
+    bool decl_only  = false;
+    decl_attributes attributes(decl_only);
+    attributes.parse(p);
+    return attributes.apply(p.env(), p.ios(), d, persistent);
+}
+
+static environment attribute_cmd(parser & p) {
+    return attribute_cmd_core(p, false);
+}
+
+static environment persistent_attribute_cmd(parser & p) {
+    p.check_token_next(get_attribute_tk(), "invalid command, 'attribute' expected");
+    return attribute_cmd_core(p, true);
+}
+
 void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("universe",     "declare a universe level", universe_cmd));
     add_cmd(r, cmd_info("universes",    "declare universe levels", universes_cmd));
@@ -964,6 +1040,8 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("protected",    "add new protected definition/theorem", protected_definition_cmd));
     add_cmd(r, cmd_info("theorem",      "add new theorem", theorem_cmd));
     add_cmd(r, cmd_info("include",      "force section parameter/variable to be included", include_cmd));
+    add_cmd(r, cmd_info("attribute",    "set declaration attributes", attribute_cmd));
+    add_cmd(r, cmd_info("persistent",   "set declaration attributes (the value is saved in .olean files)", persistent_attribute_cmd));
     add_cmd(r, cmd_info("omit",         "undo 'include' command", omit_cmd));
 }
 }
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 7905298c6..136d10aa3 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -42,7 +42,6 @@ Author: Leonardo de Moura
 #include "library/definitional/equations.h"
 #include "frontends/lean/local_decls.h"
 #include "frontends/lean/structure_cmd.h"
-#include "frontends/lean/class.h"
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/info_annotation.h"
diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp
index 695ad256d..761f417c8 100644
--- a/src/frontends/lean/tactic_hint.cpp
+++ b/src/frontends/lean/tactic_hint.cpp
@@ -14,7 +14,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/cmd_table.h"
 #include "frontends/lean/parser.h"
-#include "frontends/lean/class.h"
 #include "frontends/lean/tokens.h"
 
 namespace lean {
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 09eb8a9cd..6a3b7127b 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -89,12 +89,12 @@ void init_token_table(token_table & t) {
     char const * commands[] =
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
-         "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible",
+         "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
          "evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude",
          "import", "inductive", "record", "structure", "module", "universe", "universes",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
-         "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl",
+         "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "#erase_cache", "#projections", "#telescope_eq", nullptr};
 
     pair<char const *, char const *> aliases[] =
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 48b824c9c..a6fca3bf7 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -81,9 +81,12 @@ static name * g_instance     = nullptr;
 static name * g_priority     = nullptr;
 static name * g_coercion     = nullptr;
 static name * g_reducible    = nullptr;
+static name * g_irreducible  = nullptr;
 static name * g_parsing_only = nullptr;
 static name * g_with         = nullptr;
 static name * g_class        = nullptr;
+static name * g_multiple_instances = nullptr;
+static name * g_attribute    = nullptr;
 static name * g_prev         = nullptr;
 static name * g_scoped       = nullptr;
 static name * g_foldr        = nullptr;
@@ -178,9 +181,12 @@ void initialize_tokens() {
     g_priority     = new name("[priority");
     g_coercion     = new name("[coercion]");
     g_reducible    = new name("[reducible]");
+    g_irreducible  = new name("[irreducible]");
     g_parsing_only = new name("[parsing-only]");
+    g_attribute    = new name("attribute");
     g_with         = new name("with");
     g_class        = new name("[class]");
+    g_multiple_instances = new name("[multiple-instances]");
     g_prev         = new name("prev");
     g_scoped       = new name("scoped");
     g_foldr        = new name("foldr");
@@ -234,6 +240,9 @@ void finalize_tokens() {
     delete g_priority;
     delete g_coercion;
     delete g_reducible;
+    delete g_irreducible;
+    delete g_multiple_instances;
+    delete g_attribute;
     delete g_parsing_only;
     delete g_in;
     delete g_assign;
@@ -373,6 +382,9 @@ name const & get_instance_tk() { return *g_instance; }
 name const & get_priority_tk() { return *g_priority; }
 name const & get_coercion_tk() { return *g_coercion; }
 name const & get_reducible_tk() { return *g_reducible; }
+name const & get_irreducible_tk() { return *g_irreducible; }
+name const & get_multiple_instances_tk() { return *g_multiple_instances; }
+name const & get_attribute_tk() { return *g_attribute; }
 name const & get_parsing_only_tk() { return *g_parsing_only; }
 name const & get_class_tk() { return *g_class; }
 name const & get_with_tk() { return *g_with; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index ba5efe968..a43277c9c 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -83,6 +83,9 @@ name const & get_instance_tk();
 name const & get_priority_tk();
 name const & get_coercion_tk();
 name const & get_reducible_tk();
+name const & get_irreducible_tk();
+name const & get_multiple_instances_tk();
+name const & get_attribute_tk();
 name const & get_parsing_only_tk();
 name const & get_class_tk();
 name const & get_with_tk();
diff --git a/tests/lean/bad_class.lean b/tests/lean/bad_class.lean
index 5668cf64f..171e5bf70 100644
--- a/tests/lean/bad_class.lean
+++ b/tests/lean/bad_class.lean
@@ -1,7 +1,7 @@
 import logic
 namespace foo
 definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b
-class subsingleton
+attribute subsingleton [class]
 
 protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
 λa b, !proof_irrel
diff --git a/tests/lean/bad_coercions.lean b/tests/lean/bad_coercions.lean
index 2d54b684b..d724b3603 100644
--- a/tests/lean/bad_coercions.lean
+++ b/tests/lean/bad_coercions.lean
@@ -15,5 +15,5 @@ context
   definition foo (v : vector A n) : list A :=
   nil A
 
-  coercion foo
+  attribute foo [coercion]
 end
diff --git a/tests/lean/bad_coercions.lean.expected.out b/tests/lean/bad_coercions.lean.expected.out
index 6bca4f0e8..8d31bf5f5 100644
--- a/tests/lean/bad_coercions.lean.expected.out
+++ b/tests/lean/bad_coercions.lean.expected.out
@@ -1,2 +1,2 @@
-bad_coercions.lean:12:18: error: invalid '[coercion]' modifier, coercions cannot be defined in contexts
-bad_coercions.lean:18:11: error: invalid 'coercion' command, coercions cannot be defined in contexts or sections containing parameters
+bad_coercions.lean:12:18: error: invalid '[coercion]' attribute, coercions cannot be defined in contexts
+bad_coercions.lean:18:16: error: invalid '[coercion]' attribute, coercions cannot be defined in contexts
diff --git a/tests/lean/hott/bug_struct_level.hlean b/tests/lean/hott/bug_struct_level.hlean
index 3ddc64b04..32e9af505 100644
--- a/tests/lean/hott/bug_struct_level.hlean
+++ b/tests/lean/hott/bug_struct_level.hlean
@@ -6,7 +6,7 @@ context
   parameter {D₀ : Type}
   parameter (C  : precategory D₀)
   parameter (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type)
-  reducible compose
+  attribute compose [reducible]
 
   definition comp₁_type [reducible]  : Type :=
   Π ⦃a b c₁ d₁ c₂ d₂ : D₀⦄
diff --git a/tests/lean/run/alias1.lean b/tests/lean/run/alias1.lean
index 1ceed6318..26e4b9705 100644
--- a/tests/lean/run/alias1.lean
+++ b/tests/lean/run/alias1.lean
@@ -20,7 +20,7 @@ check foo a b
 check foo x y
 
 constant f : num → val
-coercion f
+attribute f [coercion]
 
 check foo a x
 check foo x y
diff --git a/tests/lean/run/alias2.lean b/tests/lean/run/alias2.lean
index 545ec6c47..203571a94 100644
--- a/tests/lean/run/alias2.lean
+++ b/tests/lean/run/alias2.lean
@@ -14,7 +14,7 @@ open N1
 open N2
 constants a b : num
 constant f : num → val
-coercion f
+attribute f [coercion]
 
 definition aux2 := foo a b
 check aux2
diff --git a/tests/lean/run/class11.lean b/tests/lean/run/class11.lean
index faf7b9fa6..9835105c5 100644
--- a/tests/lean/run/class11.lean
+++ b/tests/lean/run/class11.lean
@@ -1,7 +1,7 @@
 import logic
 
 constant C {A : Type} : A → Prop
-class C
+attribute C [class]
 
 constant f {A : Type} (a : A) [H : C a] : Prop
 
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index 7f54610b6..c18f91f0d 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -74,20 +74,20 @@ constant dvd : Π (x y : nat) {H : not_zero y}, nat
 constants a b : nat
 
 set_option pp.implicit true
-reducible add
+attribute add [reducible]
 check dvd a (succ b)
 check (λ H : not_zero b, dvd a b)
 check (succ zero)
 check a + (succ zero)
 check dvd a (a + (succ b))
 
-reducible [off] add
+attribute add [irreducible]
 check dvd a (a + (succ b))
 
-reducible add
+attribute add [reducible]
 check dvd a (a + (succ b))
 
-reducible [off] add
+attribute add [irreducible]
 check dvd a (a + (succ b))
 
 end nat
diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean
index 3b75c188e..aae443369 100644
--- a/tests/lean/run/class6.lean
+++ b/tests/lean/run/class6.lean
@@ -13,7 +13,8 @@ theorem inhabited_t1 : inhabited t1
 theorem inhabited_t2 : inhabited t2
 := inhabited.mk t2.mk2
 
-instance inhabited_t1 inhabited_t2
+attribute inhabited_t1 [instance]
+attribute inhabited_t2 [instance]
 
 theorem T : inhabited (t1 × t2)
 := _
diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean
index 54664b1de..2982e5679 100644
--- a/tests/lean/run/class8.lean
+++ b/tests/lean/run/class8.lean
@@ -4,7 +4,7 @@ open tactic prod
 inductive inh [class] (A : Type) : Prop :=
 intro : A -> inh A
 
-instance inh.intro
+attribute inh.intro [instance]
 
 theorem inh_elim {A : Type} {B : Prop} (H1 : inh A) (H2 : A → B) : B
 := inh.rec H2 H1
diff --git a/tests/lean/run/class_bug1.lean b/tests/lean/run/class_bug1.lean
index ecf0af9a3..4f1755ab3 100644
--- a/tests/lean/run/class_bug1.lean
+++ b/tests/lean/run/class_bug1.lean
@@ -8,7 +8,7 @@ mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
            (Π {A B : ob} {f : mor A B}, comp f id = f) →
            (Π {A B : ob} {f : mor A B}, comp id f = f) →
             category ob mor
-class category
+attribute category [class]
 
 namespace category
 context sec_cat
@@ -16,7 +16,7 @@ context sec_cat
   inductive foo :=
   mk : A → foo
 
-  class foo
+  attribute foo [class]
   parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
   definition compose := rec (λ comp id assoc idr idl, comp) Cat
   definition id := rec (λ comp id assoc idr idl, id) Cat
diff --git a/tests/lean/run/class_bug2.lean b/tests/lean/run/class_bug2.lean
index 120c729e0..247e40a97 100644
--- a/tests/lean/run/class_bug2.lean
+++ b/tests/lean/run/class_bug2.lean
@@ -8,7 +8,7 @@ mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
            (Π {A B : ob} {f : mor A B}, comp f id = f) →
            (Π {A B : ob} {f : mor A B}, comp id f = f) →
             category ob mor
-class category
+attribute category [class]
 
 namespace category
 section sec_cat
@@ -16,7 +16,7 @@ section sec_cat
   inductive foo :=
   mk : A → foo
 
-  class foo
+  attribute foo [class]
   variables {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
   definition compose := rec (λ comp id assoc idr idl, comp) Cat
   definition id := rec (λ comp id assoc idr idl, id) Cat
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index 08c753953..d1afe5947 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -24,9 +24,9 @@ constants x y : real
 constant num_to_nat : num → nat
 constant nat_to_int : nat → int
 constant int_to_real : int → real
-coercion num_to_nat
-coercion nat_to_int
-coercion int_to_real
+attribute num_to_nat [coercion]
+attribute nat_to_int [coercion]
+attribute int_to_real [coercion]
 
 set_option pp.implicit true
 set_option pp.coercions true
diff --git a/tests/lean/run/coe1.lean b/tests/lean/run/coe1.lean
index 0c6e5b094..55ff6dfa6 100644
--- a/tests/lean/run/coe1.lean
+++ b/tests/lean/run/coe1.lean
@@ -3,7 +3,7 @@ prelude
 constant A : Type.{1}
 constant B : Type.{1}
 constant f : A → B
-coercion f
+attribute f [coercion]
 constant g : B → B → B
 constants a1 a2 a3 : A
 constants b1 b2 b3 : B
diff --git a/tests/lean/run/coe11.lean b/tests/lean/run/coe11.lean
index 095b41d7c..734f7c3c7 100644
--- a/tests/lean/run/coe11.lean
+++ b/tests/lean/run/coe11.lean
@@ -17,7 +17,7 @@ my_functor.rec (λ obF homF Hid Hcomp, homF) F
 constants obC obD : Type
 constants a b : obC
 constant C : category obC
-instance C
+attribute C [instance]
 constant D : category obD
 constant F : my_functor C D
 constant m : hom a b
diff --git a/tests/lean/run/coe2.lean b/tests/lean/run/coe2.lean
index 5e51984c1..58a341154 100644
--- a/tests/lean/run/coe2.lean
+++ b/tests/lean/run/coe2.lean
@@ -12,7 +12,7 @@ namespace setoid
 
   infix `≈` := eqv
 
-  coercion carrier
+  attribute carrier [coercion]
 
   inductive morphism (s1 s2 : setoid) : Type :=
   mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
diff --git a/tests/lean/run/coe3.lean b/tests/lean/run/coe3.lean
index 0bb593bec..f4c9c52f2 100644
--- a/tests/lean/run/coe3.lean
+++ b/tests/lean/run/coe3.lean
@@ -12,7 +12,7 @@ namespace setoid
 
   infix `≈` := eqv
 
-  coercion carrier
+  attribute carrier [coercion]
 
   inductive morphism (s1 s2 : setoid) : Type :=
   mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
diff --git a/tests/lean/run/coe4.lean b/tests/lean/run/coe4.lean
index 08c4e4097..f1b2b2f06 100644
--- a/tests/lean/run/coe4.lean
+++ b/tests/lean/run/coe4.lean
@@ -17,7 +17,7 @@ namespace setoid
 
   infix `≈` := eqv
 
-  coercion carrier
+  attribute carrier [coercion]
 
   inductive morphism (s1 s2 : setoid) : Type :=
   mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean
index 41420afe8..852fc631c 100644
--- a/tests/lean/run/coe5.lean
+++ b/tests/lean/run/coe5.lean
@@ -17,7 +17,7 @@ namespace setoid
 
   infix `≈` := eqv
 
-  coercion carrier
+  attribute carrier [coercion]
 
   inductive morphism (s1 s2 : setoid) : Type :=
   mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2
diff --git a/tests/lean/run/coe7.lean b/tests/lean/run/coe7.lean
index fda2f4f3b..f98c3d8d0 100644
--- a/tests/lean/run/coe7.lean
+++ b/tests/lean/run/coe7.lean
@@ -3,7 +3,7 @@ namespace experiment
 constant nat : Type.{1}
 constant int : Type.{1}
 constant of_nat : nat → int
-coercion of_nat
+attribute of_nat [coercion]
 
 theorem tst (n : nat) : n = n :=
 have H : true, from trivial,
diff --git a/tests/lean/run/coe8.lean b/tests/lean/run/coe8.lean
index d58eb7db8..2e56be1fc 100644
--- a/tests/lean/run/coe8.lean
+++ b/tests/lean/run/coe8.lean
@@ -3,7 +3,7 @@ namespace experiment
 constant nat : Type.{1}
 constant int : Type.{1}
 constant of_nat : nat → int
-coercion of_nat
+attribute of_nat [coercion]
 constant nat_add : nat → nat → nat
 constant int_add : int → int → int
 infixl `+` := int_add
diff --git a/tests/lean/run/coe9.lean b/tests/lean/run/coe9.lean
index d0867e25e..852060c42 100644
--- a/tests/lean/run/coe9.lean
+++ b/tests/lean/run/coe9.lean
@@ -11,10 +11,10 @@ constant to_row {A : Type} {n : nat} : vector A n → matrix A 1 n
 constant to_col {A : Type} {n : nat} : vector A n → matrix A n 1
 constant to_list {A : Type} {n : nat} : vector A n → list A
 
-coercion to_row
-coercion to_col
-coercion list_to_vec
-coercion to_list
+attribute to_row [coercion]
+attribute to_col [coercion]
+attribute list_to_vec [coercion]
+attribute to_list [coercion]
 
 constant f {A : Type} {n : nat} (M : matrix A n 1) : nat
 constant g {A : Type} {n : nat} (M : matrix A 1 n) : nat
diff --git a/tests/lean/run/coesec.lean b/tests/lean/run/coesec.lean
index 30bea8630..d01e213d7 100644
--- a/tests/lean/run/coesec.lean
+++ b/tests/lean/run/coesec.lean
@@ -5,5 +5,5 @@ section
   variables {A B : Type}
   definition to_function (F : func A B) : A → B :=
   func.rec (λf, f) F
-  coercion to_function
+  attribute to_function [coercion]
 end
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index a670ae349..014d24531 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -50,7 +50,7 @@ definition rec_measure {dom codom : Type} (default : codom) (measure : dom → 
     (rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
 rec_measure_aux default measure rec_val (succ (measure x)) x
 
-multiple_instances decidable
+attribute decidable [multiple-instances]
 
 theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ)
     (rec_val : dom → (dom → codom) → codom)
diff --git a/tests/lean/run/e10.lean b/tests/lean/run/e10.lean
index 900cf9755..bf48fde64 100644
--- a/tests/lean/run/e10.lean
+++ b/tests/lean/run/e10.lean
@@ -13,7 +13,7 @@ namespace int
   constant add : int → int → int
   infixl + := add
   constant of_nat : nat → int
-  coercion of_nat
+attribute of_nat [coercion]
 end int
 
 section
diff --git a/tests/lean/run/e11.lean b/tests/lean/run/e11.lean
index e44e353d9..064a54bf3 100644
--- a/tests/lean/run/e11.lean
+++ b/tests/lean/run/e11.lean
@@ -13,7 +13,7 @@ namespace int
   constant add : int → int → int
   infixl + := add
   constant of_nat : nat → int
-  coercion of_nat
+attribute of_nat [coercion]
 end int
 
 section
diff --git a/tests/lean/run/e12.lean b/tests/lean/run/e12.lean
index c71f8dce7..7f02d5e2f 100644
--- a/tests/lean/run/e12.lean
+++ b/tests/lean/run/e12.lean
@@ -13,7 +13,7 @@ namespace int
   constant add : int → int → int
   infixl + := add
   constant of_nat : nat → int
-  coercion of_nat
+attribute of_nat [coercion]
 end int
 
 constants n m : nat.nat
diff --git a/tests/lean/run/e13.lean b/tests/lean/run/e13.lean
index ff04cea7d..a974dc486 100644
--- a/tests/lean/run/e13.lean
+++ b/tests/lean/run/e13.lean
@@ -14,7 +14,7 @@ namespace int
   infixl + := add
   constant of_nat : nat → int
   namespace coercions
-    coercion of_nat
+attribute of_nat [coercion]
   end coercions
 end int
 
diff --git a/tests/lean/run/e14.lean b/tests/lean/run/e14.lean
index 24a83e092..c70cb9e19 100644
--- a/tests/lean/run/e14.lean
+++ b/tests/lean/run/e14.lean
@@ -31,7 +31,7 @@ check vector.rec
 definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
 := vector.rec (@nil A) (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
 
-coercion vector_to_list
+attribute vector_to_list [coercion]
 
 constant f : forall {A : Type}, list A → nat
 
diff --git a/tests/lean/run/e17.lean b/tests/lean/run/e17.lean
index 7690417fd..1ddcf77f2 100644
--- a/tests/lean/run/e17.lean
+++ b/tests/lean/run/e17.lean
@@ -11,7 +11,7 @@ inductive int : Type :=
 of_nat : nat → int,
 neg : nat → int
 
-coercion int.of_nat
+attribute int.of_nat [coercion]
 
 constants n m : nat
 constants i j : int
diff --git a/tests/lean/run/e18.lean b/tests/lean/run/e18.lean
index ee92b4d63..a9f55a97a 100644
--- a/tests/lean/run/e18.lean
+++ b/tests/lean/run/e18.lean
@@ -11,7 +11,7 @@ inductive int : Type :=
 of_nat : nat → int,
 neg : nat → int
 
-coercion int.of_nat
+attribute int.of_nat [coercion]
 
 constants n m : nat
 constants i j : int
diff --git a/tests/lean/run/e6.lean b/tests/lean/run/e6.lean
index 40805acb7..167a4c5be 100644
--- a/tests/lean/run/e6.lean
+++ b/tests/lean/run/e6.lean
@@ -13,7 +13,7 @@ namespace int
   constant add : int → int → int
   infixl + := add
   constant of_nat : nat → int
-  coercion [persistent] of_nat
+  persistent attribute of_nat [coercion]
 end int
 
 open int
diff --git a/tests/lean/run/e7.lean b/tests/lean/run/e7.lean
index 1aa2c6e8a..a6079b30c 100644
--- a/tests/lean/run/e7.lean
+++ b/tests/lean/run/e7.lean
@@ -13,7 +13,7 @@ namespace int
   constant add : int → int → int
   infixl + := add
   constant of_nat : nat → int
-  coercion of_nat
+attribute of_nat [coercion]
 end int
 
 open nat
diff --git a/tests/lean/run/e8.lean b/tests/lean/run/e8.lean
index 28ac4fcd0..6891d491e 100644
--- a/tests/lean/run/e8.lean
+++ b/tests/lean/run/e8.lean
@@ -13,7 +13,7 @@ namespace int
   constant add : int → int → int
   infixl + := add
   constant of_nat : nat → int
-  coercion of_nat
+attribute of_nat [coercion]
 end int
 
 -- Open "only" the notation and declarations from the namespaces nat and int
diff --git a/tests/lean/run/e9.lean b/tests/lean/run/e9.lean
index 234758e48..75d1f0fb0 100644
--- a/tests/lean/run/e9.lean
+++ b/tests/lean/run/e9.lean
@@ -16,7 +16,7 @@ namespace int
 end int
 
 namespace int_coercions
-  coercion [persistent] int.of_nat
+  persistent attribute int.of_nat [coercion]
 end int_coercions
 
 -- Open "only" the notation and declarations from the namespaces nat and int
diff --git a/tests/lean/run/elab_failure.lean b/tests/lean/run/elab_failure.lean
index 957dc8fcf..8a8bcdf42 100644
--- a/tests/lean/run/elab_failure.lean
+++ b/tests/lean/run/elab_failure.lean
@@ -1,6 +1,6 @@
 import data.nat.basic data.bool
 open bool nat
-reducible nat.rec_on
+attribute nat.rec_on [reducible]
 definition is_eq (a b : nat) : bool :=
 nat.rec_on a
   (λ b, nat.cases_on b tt (λb₁, ff))
diff --git a/tests/lean/run/fibrant_class1.lean b/tests/lean/run/fibrant_class1.lean
index f2af1bceb..d78435a35 100644
--- a/tests/lean/run/fibrant_class1.lean
+++ b/tests/lean/run/fibrant_class1.lean
@@ -7,10 +7,10 @@ idpath : path a a
 notation a ≈ b := path a b
 
 axiom path_fibrant {A : Type'} [fA : fibrant A] (a b : A) : fibrant (path a b)
-instance [persistent] path_fibrant
+persistent attribute path_fibrant [instance]
 
 axiom imp_fibrant {A : Type'} {B : Type'} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A → B)
-instance imp_fibrant
+attribute imp_fibrant [instance]
 
 definition test {A : Type} [fA : fibrant A] {x y : A} :
 Π (z : A), y ≈ z → fibrant (x ≈ y → x ≈ z) := _
diff --git a/tests/lean/run/fibrant_class2.lean b/tests/lean/run/fibrant_class2.lean
index c1a07a549..cb5cef895 100644
--- a/tests/lean/run/fibrant_class2.lean
+++ b/tests/lean/run/fibrant_class2.lean
@@ -3,13 +3,13 @@ fibrant_mk : fibrant T
 
 axiom pi_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] :
   fibrant (Πx : A, B x)
-instance pi_fibrant
+attribute pi_fibrant [instance]
 
 inductive path {A : Type} [fA : fibrant A] (a : A) : A → Type :=
 idpath : path a a
 
 axiom path_fibrant {A : Type} [fA : fibrant A] (a b : A) : fibrant (path a b)
-instance [persistent] path_fibrant
+persistent attribute path_fibrant [instance]
 
 notation a ≈ b := path a b
 
@@ -26,7 +26,7 @@ definition test4 {A : Type} [fA : fibrant A] {x y z : A} :
   fibrant (x ≈ y → x ≈ z) := _
 
 axiom imp_fibrant {A : Type} {B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A → B)
-instance imp_fibrant
+attribute imp_fibrant [instance]
 
 definition test5 {A : Type} [fA : fibrant A] {x y : A} :
 Π (z : A), y ≈ z → fibrant (x ≈ y → x ≈ z) := _
diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean
index 50f3c82c8..f7ff60a4e 100644
--- a/tests/lean/run/group2.lean
+++ b/tests/lean/run/group2.lean
@@ -21,7 +21,7 @@ mk : Π (A : Type), group_struct A → group
 definition carrier (g : group) : Type
 := group.rec (λ c s, c) g
 
-coercion carrier
+attribute carrier [coercion]
 
 definition group_to_struct [instance] (g : group) : group_struct (carrier g)
 := group.rec (λ (A : Type) (s : group_struct A), s) g
diff --git a/tests/lean/run/group4.lean b/tests/lean/run/group4.lean
index fb5c63858..4a72cae5e 100644
--- a/tests/lean/run/group4.lean
+++ b/tests/lean/run/group4.lean
@@ -80,26 +80,26 @@ print prefix algebra.comm_monoid
 structure Semigroup :=
 mk :: (carrier : Type) (struct : semigroup carrier)
 
-coercion [persistent] Semigroup.carrier
-instance [persistent] Semigroup.struct
+persistent attribute Semigroup.carrier [coercion]
+persistent attribute Semigroup.struct [instance]
 
 structure CommSemigroup :=
 mk :: (carrier : Type) (struct : comm_semigroup carrier)
 
-coercion [persistent] CommSemigroup.carrier
-instance [persistent] CommSemigroup.struct
+persistent attribute CommSemigroup.carrier [coercion]
+persistent attribute CommSemigroup.struct [instance]
 
 structure Monoid :=
 mk :: (carrier : Type) (struct : monoid carrier)
 
-coercion [persistent] Monoid.carrier
-instance [persistent] Monoid.struct
+persistent attribute Monoid.carrier [coercion]
+persistent attribute Monoid.struct [instance]
 
 structure CommMonoid :=
 mk :: (carrier : Type) (struct : comm_monoid carrier)
 
-coercion [persistent] CommMonoid.carrier
-instance [persistent] CommMonoid.struct
+persistent attribute CommMonoid.carrier [coercion]
+persistent attribute CommMonoid.struct [instance]
 
 end algebra
 
diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean
index e087c88f0..2ea18a687 100644
--- a/tests/lean/run/group5.lean
+++ b/tests/lean/run/group5.lean
@@ -78,26 +78,26 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
 structure Semigroup :=
 (carrier : Type) (struct : semigroup carrier)
 
-coercion [persistent] Semigroup.carrier
-instance [persistent] Semigroup.struct
+persistent attribute Semigroup.carrier [coercion]
+persistent attribute Semigroup.struct [instance]
 
 structure CommSemigroup :=
 (carrier : Type) (struct : comm_semigroup carrier)
 
-coercion [persistent] CommSemigroup.carrier
-instance [persistent] CommSemigroup.struct
+persistent attribute CommSemigroup.carrier [coercion]
+persistent attribute CommSemigroup.struct [instance]
 
 structure Monoid :=
 (carrier : Type) (struct : monoid carrier)
 
-coercion [persistent] Monoid.carrier
-instance [persistent] Monoid.struct
+persistent attribute Monoid.carrier [coercion]
+persistent attribute Monoid.struct [instance]
 
 structure CommMonoid :=
 (carrier : Type) (struct : comm_monoid carrier)
 
-coercion [persistent] CommMonoid.carrier
-instance [persistent] CommMonoid.struct
+persistent attribute CommMonoid.carrier [coercion]
+persistent attribute CommMonoid.struct [instance]
 
 end algebra
 
diff --git a/tests/lean/run/impbug1.lean b/tests/lean/run/impbug1.lean
index fa8c0f450..ffb5bfc56 100644
--- a/tests/lean/run/impbug1.lean
+++ b/tests/lean/run/impbug1.lean
@@ -11,7 +11,7 @@ mk : Π (id : Π (A : ob), mor A A),
 
 definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
 
-reducible id
+attribute id [reducible]
 theorem id_left (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) (A : ob) (f : mor A A) :
      @eq (mor A A) (id ob mor Cat A) f :=
 @category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)
diff --git a/tests/lean/run/impbug2.lean b/tests/lean/run/impbug2.lean
index a56136a48..b47c81e00 100644
--- a/tests/lean/run/impbug2.lean
+++ b/tests/lean/run/impbug2.lean
@@ -14,7 +14,7 @@ constant ob  : Type.{1}
 constant mor : ob → ob → Type.{1}
 constant Cat : category ob mor
 
-reducible id
+attribute id [reducible]
 theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id ob mor Cat A) f :=
 @category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)
   (λ (id  : Π (T : ob), mor T T)
diff --git a/tests/lean/run/impbug3.lean b/tests/lean/run/impbug3.lean
index 6a7e9bd3c..2d8cf9d8f 100644
--- a/tests/lean/run/impbug3.lean
+++ b/tests/lean/run/impbug3.lean
@@ -15,7 +15,7 @@ mk : Π (id : Π (A : ob), mor A A),
 definition id (Cat : category) := category.rec (λ id idl, id) Cat
 constant Cat : category
 
-reducible id
+attribute id [reducible]
 theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id Cat A) f :=
 @category.rec (λ (C : category), @eq (mor A A) (id C A) f)
   (λ (id  : Π (T : ob), mor T T)
diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean
index a107a712d..527df7699 100644
--- a/tests/lean/run/list_elab1.lean
+++ b/tests/lean/run/list_elab1.lean
@@ -23,7 +23,7 @@ list.rec Hnil Hind l
 definition concat {T : Type} (s t : list T) : list T :=
 list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
 
-reducible concat
+attribute concat [reducible]
 theorem concat_nil {T : Type} (t : list T) : concat t nil = t :=
 list_induction_on t (eq.refl (concat nil nil))
   (take (x : T) (l : list T) (H : concat l nil = l),
diff --git a/tests/lean/run/nat_coe.lean b/tests/lean/run/nat_coe.lean
index 2696d2161..bb9c5280d 100644
--- a/tests/lean/run/nat_coe.lean
+++ b/tests/lean/run/nat_coe.lean
@@ -10,7 +10,7 @@ constant int_add : int → int → int
 infixl `+` := int_add
 
 constant of_nat : nat → int
-coercion of_nat
+attribute of_nat [coercion]
 
 constants a b : nat
 constants i j : int
diff --git a/tests/lean/run/nateq.lean b/tests/lean/run/nateq.lean
index 54fdb2e0e..27cbd6fbf 100644
--- a/tests/lean/run/nateq.lean
+++ b/tests/lean/run/nateq.lean
@@ -1,6 +1,6 @@
 import data.nat.basic data.bool
 open bool nat eq.ops
-reducible nat.rec_on
+attribute nat.rec_on [reducible]
 
 definition is_eq (a b : nat) : bool :=
 nat.rec_on a
diff --git a/tests/lean/run/opaque_hint_bug.lean b/tests/lean/run/opaque_hint_bug.lean
index 70ef84fb4..e94ac433d 100644
--- a/tests/lean/run/opaque_hint_bug.lean
+++ b/tests/lean/run/opaque_hint_bug.lean
@@ -9,5 +9,5 @@ section
   definition concat (s t : list T) : list T
   := list.rec t (fun x l u, list.cons x u) s
 
-  reducible concat
+  attribute concat [reducible]
 end
diff --git a/tests/lean/run/private_names.lean b/tests/lean/run/private_names.lean
index c194ab6f8..b71139030 100644
--- a/tests/lean/run/private_names.lean
+++ b/tests/lean/run/private_names.lean
@@ -3,7 +3,7 @@ section
   private definition foo : inhabited Prop :=
   inhabited.mk false
 
-  instance [priority 1000] foo
+  attribute foo [instance] [priority 1000]
 
   example : default Prop = false :=
   rfl
diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean
index 6413189f2..944566d9f 100644
--- a/tests/lean/run/tactic23.lean
+++ b/tests/lean/run/tactic23.lean
@@ -17,7 +17,7 @@ definition pos_num_to_nat (n : pos_num) : nat
 := pos_num.rec one (λ n r, r + r) (λ n r, r + r + one) n
 definition num_to_nat (n : num) : nat
 := num.rec zero (λ n, pos_num_to_nat n) n
-coercion num_to_nat
+attribute num_to_nat [coercion]
 
 -- Now we can write 2 + 3, the coercion will be applied
 check 2 + 3
diff --git a/tests/lean/run/trans.lean b/tests/lean/run/trans.lean
index 8c6a02cd7..be1a6d377 100644
--- a/tests/lean/run/trans.lean
+++ b/tests/lean/run/trans.lean
@@ -11,7 +11,7 @@ definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a)
 theorem transport_refl {A : Type} {a : A} {P : A → Type} (H : P a) : transport (refl a) H = H
 := refl H
 
-reducible [off] transport
+attribute transport [irreducible]
 theorem transport_proof_irrel {A : Type} {a b : A} {P : A → Type} (p1 p2 : a = b) (H : P a) : transport p1 H = transport p2 H
 := refl (transport p1 H)
 
diff --git a/tests/lean/sec2.lean b/tests/lean/sec2.lean
index efae2f972..c0f965a0f 100644
--- a/tests/lean/sec2.lean
+++ b/tests/lean/sec2.lean
@@ -5,7 +5,7 @@ constant g : B → B
 constant a : A
 
 namespace foo
-  coercion f
+  attribute f [coercion]
   print coercions
   check g a
 end foo
@@ -13,7 +13,7 @@ end foo
 check g a -- Error
 
 section boo
-  coercion f
+  attribute f [coercion]
   print coercions
   check g a
 end boo
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 6a4648e33..632e862b6 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -61,7 +61,7 @@ list_induction_on t (refl _)
   (take (x : T) (l : list T) (H : concat l nil = l),
     H ▸ (refl (cons x (concat l nil))))
 
-reducible concat
+attribute concat [reducible]
 theorem concat_nil2 (t : list T) : t ++ nil = t :=
 list_induction_on t (refl _)
   (take (x : T) (l : list T) (H : concat l nil = l),