From 03e4fd1038cb99d7f8b997145a3b54d39928fced Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Sep 2016 11:13:54 -0700
Subject: [PATCH] feat(frontends/lean,library): cleanup instance cmd, and use
 'meta instance'

---
 library/init/meta/environment.lean     |   6 +-
 library/init/meta/exceptional.lean     |   6 +-
 library/init/meta/expr.lean            |   3 +-
 library/init/meta/format.lean          | 105 ++++++++++---------------
 library/init/meta/fun_info.lean        |   9 +--
 library/init/meta/level.lean           |  20 ++---
 library/init/meta/name.lean            |  20 ++---
 library/init/meta/occurrences.lean     |  15 ++--
 library/init/meta/options.lean         |  10 +--
 library/init/meta/pexpr.lean           |  15 ++--
 library/init/meta/rb_map.lean          |   6 +-
 library/init/meta/tactic.lean          |  40 ++++------
 src/frontends/lean/decl_attributes.cpp |   7 +-
 src/frontends/lean/decl_attributes.h   |   6 +-
 src/frontends/lean/decl_cmds.cpp       |  22 ++----
 src/frontends/lean/decl_util.h         |   1 +
 src/frontends/lean/definition_cmds.cpp |   4 +-
 src/frontends/lean/inductive_cmds.cpp  |   2 -
 tests/lean/elab3.lean.expected.out     |   2 +-
 19 files changed, 116 insertions(+), 183 deletions(-)

diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean
index 1067bcd4ee..b4bf39739d 100644
--- a/library/init/meta/environment.lean
+++ b/library/init/meta/environment.lean
@@ -70,10 +70,8 @@ match (refl_for env (const_name (get_app_fn e))) with
 end
 end environment
 
-attribute [instance]
-meta definition environment.has_to_string : has_to_string environment :=
+meta instance : has_to_string environment :=
 ⟨λ e, "[environment]"⟩
 
-attribute [instance]
-meta definition environment.is_inhabited : inhabited environment :=
+meta instance : inhabited environment :=
 ⟨environment.mk_std 0⟩
diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean
index 8845677885..65342e4aa3 100644
--- a/library/init/meta/exceptional.lean
+++ b/library/init/meta/exceptional.lean
@@ -22,8 +22,7 @@ protected meta definition exceptional.to_string : exceptional A → string
 | (success a)       := to_string a
 | (exception .A e) := "Exception: " ++ to_string (e options.mk)
 
-attribute [instance]
-protected meta definition exceptional.has_to_string : has_to_string (exceptional A) :=
+meta instance : has_to_string (exceptional A) :=
 has_to_string.mk exceptional.to_string
 end
 
@@ -51,6 +50,5 @@ meta definition fail (f : format) : exceptional A :=
 exception A (λ u, f)
 end exceptional
 
-attribute [instance]
-meta definition exceptional.is_monad : monad exceptional :=
+meta instance : monad exceptional :=
 ⟨@exceptional.fmap, @exceptional.return, @exceptional.bind⟩
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 9e8d8a5d96..9199c46ca3 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -39,8 +39,7 @@ 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 :=
+meta instance : has_to_string expr :=
 has_to_string.mk expr.to_string
 
 meta constant expr.hash : expr → nat
diff --git a/library/init/meta/format.lean b/library/init/meta/format.lean
index 251be53b3c..acaf116421 100644
--- a/library/init/meta/format.lean
+++ b/library/init/meta/format.lean
@@ -27,36 +27,29 @@ meta constant format.of_options      : options → format
 meta constant format.is_nil          : format → bool
 meta constant trace_fmt {A : Type u} : format → (unit → A) → A
 
+meta instance : inhabited format :=
+⟨format.space⟩
 
-attribute [instance]
-meta definition format.is_inhabited : inhabited format :=
-inhabited.mk format.space
+meta instance : has_append format :=
+⟨format.compose⟩
 
-attribute [instance]
-meta definition format_has_append : has_append format :=
-has_append.mk format.compose
-
-attribute [instance]
-meta definition format_has_to_string : has_to_string format :=
-has_to_string.mk (λ f, format.to_string f options.mk)
+meta instance : has_to_string format :=
+⟨λ f, format.to_string f options.mk⟩
 
 structure [class] has_to_format (A : Type u) :=
 (to_format : A → format)
 
-attribute [instance]
-meta definition format_has_to_format : has_to_format format :=
-has_to_format.mk id
+meta instance : has_to_format format :=
+⟨id⟩
 
 meta definition to_fmt {A : Type u} [has_to_format A] : A → format :=
 has_to_format.to_format
 
-attribute [instance]
-meta definition coe_nat_to_format : has_coe nat format :=
-has_coe.mk format.of_nat
+meta instance nat_to_format : has_coe nat format :=
+⟨format.of_nat⟩
 
-attribute [instance]
-meta definition coe_string_to_format : has_coe string format :=
-has_coe.mk format.of_string
+meta instance string_to_format : has_coe string format :=
+⟨format.of_string⟩
 
 open format list
 
@@ -64,29 +57,23 @@ meta definition format.when {A : Type u} [has_to_format A] : bool → A → form
 | tt a := to_fmt a
 | ff a := nil
 
-attribute [instance]
-meta definition options.has_to_format : has_to_format options :=
-has_to_format.mk (λ o, format.of_options o)
+meta instance : has_to_format options :=
+⟨λ o, format.of_options o⟩
 
-attribute [instance]
-meta definition bool.has_to_format : has_to_format bool :=
-has_to_format.mk (λ b, if b then of_string "tt" else of_string "ff")
+meta instance : has_to_format bool :=
+⟨λ b, if b then of_string "tt" else of_string "ff"⟩
 
-attribute [instance]
-meta definition decidable.has_to_format {p : Prop} : has_to_format (decidable p) :=
-has_to_format.mk (λ b : decidable p, @ite p b _ (of_string "tt") (of_string "ff"))
+meta instance {p : Prop} : has_to_format (decidable p) :=
+⟨λ b : decidable p, @ite p b _ (of_string "tt") (of_string "ff")⟩
 
-attribute [instance]
-meta definition string.has_to_format : has_to_format string :=
-has_to_format.mk (λ s, format.of_string s)
+meta instance : has_to_format string :=
+⟨λ s, format.of_string s⟩
 
-attribute [instance]
-meta definition nat.has_to_format : has_to_format nat :=
-has_to_format.mk (λ n, format.of_nat n)
+meta instance : has_to_format nat :=
+⟨λ n, format.of_nat n⟩
 
-attribute [instance]
-meta definition char.has_to_format : has_to_format char :=
-has_to_format.mk (λ c : char, format.of_string [c])
+meta instance : has_to_format char :=
+⟨λ c : char, format.of_string [c]⟩
 
 meta definition list.to_format_aux {A : Type u} [has_to_format A] : bool → list A → format
 | b  []      := to_fmt ""
@@ -97,50 +84,42 @@ meta definition list.to_format {A : Type u} [has_to_format A] : list A → forma
 | []      := to_fmt "[]"
 | (x::xs) := to_fmt "[" ++ group (nest 1 (list.to_format_aux tt (x::xs))) ++ to_fmt "]"
 
-attribute [instance]
-meta definition list.has_to_format {A : Type u} [has_to_format A] : has_to_format (list A) :=
-has_to_format.mk list.to_format
+meta instance {A : Type u} [has_to_format A] : has_to_format (list A) :=
+⟨list.to_format⟩
 
 attribute [instance] string.has_to_format
 
-attribute [instance]
-meta definition name.has_to_format : has_to_format name :=
-has_to_format.mk (λ n, to_fmt (to_string n))
+meta instance : has_to_format name :=
+⟨λ n, to_fmt (to_string n)⟩
 
-attribute [instance]
-meta definition unit.has_to_format : has_to_format unit :=
-has_to_format.mk (λ u, to_fmt "()")
+meta instance : has_to_format unit :=
+⟨λ u, to_fmt "()"⟩
 
-attribute [instance]
-meta definition option.has_to_format {A : Type u} [has_to_format A] : has_to_format (option A) :=
-has_to_format.mk (λ o, option.cases_on o
+meta instance {A : Type u} [has_to_format A] : has_to_format (option A) :=
+⟨λ o, option.cases_on o
   (to_fmt "none")
-  (λ a, to_fmt "(some " ++ nest 6 (to_fmt a) ++ to_fmt ")"))
+  (λ a, to_fmt "(some " ++ nest 6 (to_fmt a) ++ to_fmt ")")⟩
 
-attribute [instance]
-meta definition sum.has_to_format {A : Type u} {B : Type v} [has_to_format A] [has_to_format B] : has_to_format (sum A B) :=
-has_to_format.mk (λ s, sum.cases_on s
+meta instance {A : Type u} {B : Type v} [has_to_format A] [has_to_format B] : has_to_format (sum A B) :=
+⟨λ s, sum.cases_on s
   (λ a, to_fmt "(inl " ++ nest 5 (to_fmt a) ++ to_fmt ")")
-  (λ b, to_fmt "(inr " ++ nest 5 (to_fmt b) ++ to_fmt ")"))
+  (λ b, to_fmt "(inr " ++ nest 5 (to_fmt b) ++ to_fmt ")")⟩
 
 open prod
 
-attribute [instance]
-meta definition prod.has_to_format {A : Type u} {B : Type v} [has_to_format A] [has_to_format B] : has_to_format (prod A B) :=
-has_to_format.mk (λ p, group (nest 1 (to_fmt "(" ++ to_fmt (fst p) ++ to_fmt "," ++ line ++ to_fmt (snd p) ++ to_fmt ")")))
+meta instance {A : Type u} {B : Type v} [has_to_format A] [has_to_format B] : has_to_format (prod A B) :=
+⟨λ p, group (nest 1 (to_fmt "(" ++ to_fmt (fst p) ++ to_fmt "," ++ line ++ to_fmt (snd p) ++ to_fmt ")"))⟩
 
 open sigma
 
-attribute [instance]
-meta definition sigma.has_to_format {A : Type u} {B : A → Type v} [has_to_format A] [s : ∀ x, has_to_format (B x)]
+meta instance {A : Type u} {B : A → Type v} [has_to_format A] [s : ∀ x, has_to_format (B x)]
                                           : has_to_format (sigma B) :=
-has_to_format.mk (λ p, group (nest 1 (to_fmt "⟨"  ++ to_fmt (fst p) ++ to_fmt "," ++ line ++ to_fmt (snd p) ++ to_fmt "⟩")))
+⟨λ p, group (nest 1 (to_fmt "⟨"  ++ to_fmt (fst p) ++ to_fmt "," ++ line ++ to_fmt (snd p) ++ to_fmt "⟩"))⟩
 
 open subtype
 
-attribute [instance]
-meta definition subtype.has_to_format {A : Type u} {P : A → Prop} [has_to_format A] : has_to_format (subtype P) :=
-has_to_format.mk (λ s, to_fmt (elt_of s))
+meta instance {A : Type u} {P : A → Prop} [has_to_format A] : has_to_format (subtype P) :=
+⟨λ s, to_fmt (elt_of s)⟩
 
 meta definition format.bracket : string → string → format → format
 | o c f := to_fmt o ++ nest (utf8_length o) f ++ to_fmt c
diff --git a/library/init/meta/fun_info.lean b/library/init/meta/fun_info.lean
index 58ecea41b2..e6e6ed842e 100644
--- a/library/init/meta/fun_info.lean
+++ b/library/init/meta/fun_info.lean
@@ -34,8 +34,7 @@ group ∘ cbrace $
   when d  "has_fwd_deps" +++
   when (to_bool (length ds > 0)) (to_fmt "back_deps := " ++ to_fmt ds)
 
-attribute [instance]
-meta definition param_info.has_to_format : has_to_format param_info :=
+meta instance : has_to_format param_info :=
 has_to_format.mk param_info.to_format
 
 structure fun_info :=
@@ -48,8 +47,7 @@ group ∘ dcbrace $
   ppfield "params" ps +++
   ppfield "result_deps" ds
 
-attribute [instance]
-meta definition fun_info_has_to_format : has_to_format fun_info :=
+meta instance : has_to_format fun_info :=
 has_to_format.mk fun_info_to_format
 
 /-
@@ -84,8 +82,7 @@ group ∘ cbrace $
   when s  "specialized" +++
   when ss "subsingleton"
 
-attribute [instance]
-meta definition subsingleton_info_has_to_format : has_to_format subsingleton_info :=
+meta instance : has_to_format subsingleton_info :=
 has_to_format.mk subsingleton_info_to_format
 
 namespace tactic
diff --git a/library/init/meta/level.lean b/library/init/meta/level.lean
index 65e74aa9e0..433792a2e8 100644
--- a/library/init/meta/level.lean
+++ b/library/init/meta/level.lean
@@ -16,9 +16,8 @@ inductive level
 | global : name → level
 | mvar   : name → level
 
-attribute [instance]
-definition level.is_inhabited : inhabited level :=
-inhabited.mk level.zero
+meta instance : inhabited level :=
+⟨level.zero⟩
 
 /- TODO(Leo): provide a definition in Lean. -/
 meta constant level.has_decidable_eq : decidable_eq level
@@ -43,17 +42,14 @@ if level.lt a b = bool.tt then ordering.lt
 else if a = b then ordering.eq
 else ordering.gt
 
-attribute [instance]
-meta definition level.has_to_string : has_to_string level :=
-has_to_string.mk level.to_string
+meta instance : has_to_string level :=
+⟨level.to_string⟩
 
-attribute [instance]
-meta definition level.has_to_format : has_to_format level :=
-has_to_format.mk (λ l, level.to_format l options.mk)
+meta instance : has_to_format level :=
+⟨λ l, level.to_format l options.mk⟩
 
-attribute [instance]
-meta definition level.has_to_cmp : has_ordering level :=
-has_ordering.mk level.cmp
+meta instance : has_ordering level :=
+⟨level.cmp⟩
 
 meta definition level.of_nat : nat → level
 | 0            := level.zero
diff --git a/library/init/meta/name.lean b/library/init/meta/name.lean
index 352de2de13..441c79f61c 100644
--- a/library/init/meta/name.lean
+++ b/library/init/meta/name.lean
@@ -12,9 +12,8 @@ inductive name
 | mk_string  : string → name → name
 | mk_numeral : unsigned → name → name
 
-attribute [instance]
-definition name.is_inhabited : inhabited name :=
-inhabited.mk name.anonymous
+instance : inhabited name :=
+⟨name.anonymous⟩
 
 definition mk_str_name (n : name) (s : string) : name :=
 name.mk_string s n
@@ -25,9 +24,8 @@ name.mk_numeral (unsigned.of_nat v) n
 definition mk_simple_name (s : string) : name :=
 mk_str_name name.anonymous s
 
-attribute [instance]
-definition coe_string_to_name : has_coe string name :=
-has_coe.mk mk_simple_name
+instance string_to_name : has_coe string name :=
+⟨mk_simple_name⟩
 
 infix ` <.> `:65 := mk_str_name
 
@@ -45,9 +43,8 @@ definition name.to_string : name → string
 | (mk_string s n)          := name.to_string n ++ "." ++ s
 | (mk_numeral v n)         := name.to_string n ++ "." ++ to_string v
 
-attribute [instance]
-definition name.has_to_string : has_to_string name :=
-has_to_string.mk name.to_string
+instance : has_to_string name :=
+⟨name.to_string⟩
 
 /- TODO(Leo): provide a definition in Lean. -/
 meta constant name.has_decidable_eq : decidable_eq name
@@ -57,9 +54,8 @@ meta constant name.lex_cmp : name → name → ordering
 
 attribute [instance] name.has_decidable_eq
 
-attribute [instance]
-meta definition name_has_ordering : has_ordering name :=
-has_ordering.mk name.cmp
+meta instance : has_ordering name :=
+⟨name.cmp⟩
 
 /- (name.append_after n i) return a name of the form n_i -/
 meta constant name.append_after : name → nat → name
diff --git a/library/init/meta/occurrences.lean b/library/init/meta/occurrences.lean
index 5c66328dce..b669416b03 100644
--- a/library/init/meta/occurrences.lean
+++ b/library/init/meta/occurrences.lean
@@ -25,26 +25,23 @@ inductive occurrences
 
 open occurrences
 
-attribute [instance]
-definition occurrences_is_inhabited : inhabited occurrences :=
-inhabited.mk all
+instance : inhabited occurrences :=
+⟨all⟩
 
 definition occurrences_to_string : occurrences → string
 | occurrences.all     := "*"
 | (occurrences.pos l) := to_string l
 | (occurrences.neg l) := "-" ++ to_string l
 
-attribute [instance]
-definition occurrences_has_to_string : has_to_string occurrences :=
-has_to_string.mk occurrences_to_string
+instance : has_to_string occurrences :=
+⟨occurrences_to_string⟩
 
 meta definition occurrences_to_format : occurrences → format
 | occurrences.all     := to_fmt "*"
 | (occurrences.pos l) := to_fmt l
 | (occurrences.neg l) := to_fmt "-" ++ to_fmt l
 
-attribute [instance]
-meta definition occurrences_has_to_format : has_to_format occurrences :=
-has_to_format.mk occurrences_to_format
+meta instance : has_to_format occurrences :=
+⟨occurrences_to_format⟩
 
 open decidable tactic
diff --git a/library/init/meta/options.lean b/library/init/meta/options.lean
index d49a2ef483..c61af0e59d 100644
--- a/library/init/meta/options.lean
+++ b/library/init/meta/options.lean
@@ -22,10 +22,8 @@ meta constant options.has_decidable_eq  : decidable_eq options
 
 attribute [instance] options.has_decidable_eq
 
-attribute [instance]
-meta definition options.has_add : has_add options :=
-has_add.mk options.join
+meta instance : has_add options :=
+⟨options.join⟩
 
-attribute [instance]
-meta definition options.is_inhabited : inhabited options :=
-inhabited.mk options.mk
+meta instance : inhabited options :=
+⟨options.mk⟩
diff --git a/library/init/meta/pexpr.lean b/library/init/meta/pexpr.lean
index 2c83a121ec..03dbb217b5 100644
--- a/library/init/meta/pexpr.lean
+++ b/library/init/meta/pexpr.lean
@@ -13,9 +13,8 @@ protected meta constant pexpr.of_expr : expr → pexpr
 protected meta constant pexpr.subst   : pexpr → pexpr → pexpr
 
 meta constant pexpr.to_string : pexpr → string
-attribute [instance]
-meta definition pexpr.has_to_string : has_to_string pexpr :=
-has_to_string.mk pexpr.to_string
+meta instance : has_to_string pexpr :=
+⟨pexpr.to_string⟩
 
 structure [class] has_to_pexpr (A : Type u) :=
 (to_pexpr : A → pexpr)
@@ -23,10 +22,8 @@ structure [class] has_to_pexpr (A : Type u) :=
 meta definition to_pexpr {A : Type u} [has_to_pexpr A] : A → pexpr :=
 has_to_pexpr.to_pexpr
 
-attribute [instance]
-meta definition pexpr.has_to_pexpr : has_to_pexpr pexpr :=
-has_to_pexpr.mk id
+meta instance : has_to_pexpr pexpr :=
+⟨id⟩
 
-attribute [instance]
-meta definition expr.has_to_pexpr : has_to_pexpr expr :=
-has_to_pexpr.mk pexpr.of_expr
+meta instance : has_to_pexpr expr :=
+⟨pexpr.of_expr⟩
diff --git a/library/init/meta/rb_map.lean b/library/init/meta/rb_map.lean
index 7ba33a3e31..46aa919fba 100644
--- a/library/init/meta/rb_map.lean
+++ b/library/init/meta/rb_map.lean
@@ -57,8 +57,7 @@ variables {key : Type} {data : Type} [has_to_format key] [has_to_format data]
 private meta definition format_key_data (k : key) (d : data) (first : bool) : format :=
 (if first then to_fmt "" else to_fmt "," ++ line) ++ to_fmt k ++ space ++ to_fmt "←" ++ space ++ to_fmt d
 
-attribute [instance]
-meta definition rb_map_has_to_format : has_to_format (rb_map key data) :=
+meta instance : has_to_format (rb_map key data) :=
 ⟨λ m, group $ to_fmt "⟨" ++ nest 1 (fst (fold m (to_fmt "", tt) (λ k d p, (fst p ++ format_key_data k d (snd p), ff)))) ++
               to_fmt "⟩"⟩
 end
@@ -68,8 +67,7 @@ variables {key : Type} {data : Type} [has_to_string key] [has_to_string data]
 private meta definition key_data_to_string (k : key) (d : data) (first : bool) : string :=
 (if first then "" else ", ") ++ to_string k ++ " ← " ++ to_string d
 
-attribute [instance]
-meta definition rb_map_has_to_string : has_to_string (rb_map key data) :=
+meta instance : has_to_string (rb_map key data) :=
 ⟨λ m, "⟨" ++ (fst (fold m ("", tt) (λ k d p, (fst p ++ key_data_to_string k d (snd p), ff)))) ++ "⟩"⟩
 end
 
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index c42fdb30fe..8b599dcea2 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -19,9 +19,8 @@ meta constant get_options : tactic_state → options
 meta constant set_options : tactic_state → options → tactic_state
 end tactic_state
 
-attribute [instance]
-meta definition tactic_state.has_to_format : has_to_format tactic_state :=
-has_to_format.mk tactic_state.to_format
+meta instance : has_to_format tactic_state :=
+⟨tactic_state.to_format⟩
 
 inductive tactic_result (A : Type)
 | success   : A → tactic_state → tactic_result
@@ -37,9 +36,8 @@ meta definition tactic_result_to_string : tactic_result A → string
 | (success a s)   := to_string a
 | (exception .A e s) := "Exception: " ++ to_string (e ())
 
-attribute [instance]
-meta definition tactic_result_has_to_string : has_to_string (tactic_result A) :=
-has_to_string.mk tactic_result_to_string
+meta instance : has_to_string (tactic_result A) :=
+⟨tactic_result_to_string⟩
 end
 
 attribute [reducible]
@@ -73,9 +71,8 @@ meta definition tactic_orelse {A : Type} (t₁ t₂ : tactic A) : tactic A :=
      (exception A))
 end
 
-attribute [instance]
-meta definition tactic_is_monad : monad tactic :=
-monad.mk @tactic_fmap @tactic_return @tactic_bind
+meta instance : monad tactic :=
+⟨@tactic_fmap, @tactic_return, @tactic_bind⟩
 
 meta definition tactic.fail {A B : Type} [has_to_format B] (msg : B) : tactic A :=
 λ s, exception A (λ u, to_fmt msg) s
@@ -83,9 +80,8 @@ meta definition tactic.fail {A B : Type} [has_to_format B] (msg : B) : tactic A
 meta definition tactic.failed {A : Type} : tactic A :=
 tactic.fail "failed"
 
-attribute [instance]
-meta definition tactic_is_alternative : alternative tactic :=
-alternative.mk @tactic_fmap (λ A a s, success a s) (@fapp _ _) @tactic.failed @tactic_orelse
+meta instance : alternative tactic :=
+⟨@tactic_fmap, (λ A a s, success a s), (@fapp _ _), @tactic.failed, @tactic_orelse⟩
 
 namespace tactic
 variables {A : Type}
@@ -150,9 +146,8 @@ do s ← tactic.read, return (tactic_state.format_expr s e)
 structure [class] has_to_tactic_format (A : Type) :=
 (to_tactic_format : A → tactic format)
 
-attribute [instance]
-meta definition expr_has_to_tactic_format : has_to_tactic_format expr :=
-has_to_tactic_format.mk tactic_format_expr
+meta instance : has_to_tactic_format expr :=
+⟨tactic_format_expr⟩
 
 meta definition tactic.pp {A : Type} [has_to_tactic_format A] : A → tactic format :=
 has_to_tactic_format.to_tactic_format
@@ -172,13 +167,11 @@ meta definition list_to_tactic_format {A : Type} [has_to_tactic_format A] : list
   f ← list_to_tactic_format_aux tt (x::xs),
   return $ to_fmt "[" ++ group (nest 1 f) ++ to_fmt "]"
 
-attribute [instance]
-meta definition list_has_to_tactic_format {A : Type} [has_to_tactic_format A] : has_to_tactic_format (list A) :=
-has_to_tactic_format.mk list_to_tactic_format
+meta instance {A : Type} [has_to_tactic_format A] : has_to_tactic_format (list A) :=
+⟨list_to_tactic_format⟩
 
-attribute [instance]
-meta definition has_to_format_to_has_to_tactic_format (A : Type) [has_to_format A] : has_to_tactic_format A :=
-has_to_tactic_format.mk ((λ x, return x) ∘ to_fmt)
+meta instance has_to_format_to_has_to_tactic_format (A : Type) [has_to_format A] : has_to_tactic_format A :=
+⟨(λ x, return x) ∘ to_fmt⟩
 
 namespace tactic
 open tactic_state
@@ -519,9 +512,8 @@ do g::gs ← get_goals | failed,
    gs' ← get_goals,
    set_goals (gs' ++ gs)
 
-attribute [instance]
-meta definition tactic_has_andthen : has_andthen (tactic unit) :=
-has_andthen.mk seq
+meta instance : has_andthen (tactic unit) :=
+⟨seq⟩
 
 /- Applies tac if c holds -/
 meta definition when (c : Prop) [decidable c] (tac : tactic unit) : tactic unit :=
diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index dcabf31199..f5ba31e4ee 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -81,9 +81,10 @@ void decl_attributes::parse(parser & p) {
     }
 }
 
-void decl_attributes::set_instance_cmd(environment const & env) {
-    auto const & attr = get_attribute(env, "instance");
-    m_instance_cmd = true;
+void decl_attributes::set_attribute(environment const & env, name const & attr_name) {
+    if (!is_attribute(env, attr_name))
+        throw exception(sstream() << "unknown attribute [" << attr_name << "]");
+    auto const & attr = get_attribute(env, attr_name);
     m_entries = cons({&attr, get_default_attr_data()}, m_entries);
 }
 
diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index 61ba51641f..a6e1055bb8 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -21,13 +21,11 @@ public:
 private:
     bool               m_persistent;
     bool               m_parsing_only;
-    bool               m_instance_cmd;
     list<entry>        m_entries;
     optional<unsigned> m_prio;
 public:
-    decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false), m_instance_cmd(false) {}
-    void set_instance_cmd(environment const & env);
-    bool is_instance_cmd() const { return m_instance_cmd; }
+    decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {}
+    void set_attribute(environment const & env, name const & attr_name);
     void parse(parser & p);
     environment apply(environment env, io_state const & ios, name const & d) const;
     list<entry> const & get_entries() const { return m_entries; }
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 930cd74674..1399057d42 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -466,6 +466,10 @@ static environment definition_cmd_ex(parser & p, decl_attributes const & attribu
     } else if (p.curr_is_token_or_id(get_theorem_tk())) {
         p.next();
         kind = Theorem;
+    } else if (!modifiers.m_is_private && !modifiers.m_is_protected && p.curr_is_token_or_id(get_instance_tk())) {
+        p.next();
+        modifiers.m_is_protected = true;
+        modifiers.m_is_instance  = true;
     } else {
         throw parser_error("invalid definition/theorem, 'definition' or 'theorem' expected", p.pos());
     }
@@ -482,20 +486,6 @@ static environment example_cmd(parser & p) {
     return p.env();
 }
 
-static environment instance_cmd_ex(parser & p, decl_attributes attributes) {
-    attributes.set_instance_cmd(p.env());
-    decl_modifiers modifiers;
-    modifiers.m_is_protected = true;
-    return definition_cmd_core(p, Definition, modifiers, attributes);
-}
-
-
-static environment instance_cmd(parser & p) {
-    bool persistent = true;
-    decl_attributes attributes(persistent);
-    return instance_cmd_ex(p, attributes);
-}
-
 static environment attribute_cmd_core(parser & p, bool persistent) {
     buffer<name> ds;
     decl_attributes attributes(persistent);
@@ -509,8 +499,6 @@ static environment attribute_cmd_core(parser & p, bool persistent) {
                 return inductive_cmd_ex(p, attributes);
             } else  if (p.curr_is_token_or_id(get_structure_tk())) {
                 return structure_cmd_ex(p, attributes, false);
-            } else if (p.curr_is_token_or_id(get_instance_tk())) {
-                return instance_cmd_ex(p, attributes);
             } else {
                 return definition_cmd_ex(p, attributes);
             }
@@ -598,7 +586,7 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("private",         "add new private definition/theorem", definition_cmd, false));
     add_cmd(r, cmd_info("protected",       "add new protected definition/theorem/variable", definition_cmd, false));
     add_cmd(r, cmd_info("theorem",         "add new theorem", definition_cmd, false));
-    add_cmd(r, cmd_info("instance",        "add new instance", instance_cmd));
+    add_cmd(r, cmd_info("instance",        "add new instance", definition_cmd, false));
     add_cmd(r, cmd_info("example",         "add new example", example_cmd));
     add_cmd(r, cmd_info("reveal",          "reveal given theorems", reveal_cmd));
     add_cmd(r, cmd_info("include",         "force section parameter/variable to be included", include_cmd));
diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h
index 67cd5635e9..99812126a3 100644
--- a/src/frontends/lean/decl_util.h
+++ b/src/frontends/lean/decl_util.h
@@ -20,6 +20,7 @@ struct decl_modifiers {
     bool m_is_meta{false};
     bool m_is_mutual{false};
     bool m_is_noncomputable{false};
+    bool m_is_instance{false};
 };
 
 /** \brief Parse explict universe parameters of the form:
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index b7f090adea..398b43d7db 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -379,7 +379,9 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     auto header_pos = p.pos();
     declaration_info_scope scope(p, kind, modifiers);
     bool is_example  = (kind == def_cmd_kind::Example);
-    bool is_instance = attrs.is_instance_cmd();
+    bool is_instance = modifiers.m_is_instance;
+    if (is_instance)
+        attrs.set_attribute(p.env(), "instance");
     std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance);
     elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
     buffer<expr> new_params;
diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index cc61311f40..f12917012a 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -520,13 +520,11 @@ public:
 };
 
 environment inductive_cmd_ex(parser & p, decl_attributes const & attrs) {
-    lean_assert(p.curr_is_token_or_id(get_inductive_tk()));
     p.next();
     return inductive_cmd_fn(p, attrs).inductive_cmd();
 }
 
 environment mutual_inductive_cmd_ex(parser & p, decl_attributes const & attrs) {
-    lean_assert(p.curr_is_token_or_id(get_mutual_inductive_tk()));
     p.next();
     return inductive_cmd_fn(p, attrs).mutual_inductive_cmd();
 }
diff --git a/tests/lean/elab3.lean.expected.out b/tests/lean/elab3.lean.expected.out
index 98d7ef88a0..da59fa2e3a 100644
--- a/tests/lean/elab3.lean.expected.out
+++ b/tests/lean/elab3.lean.expected.out
@@ -1 +1 @@
-@monad.and_then.{1 1} unit unit tactic tactic_is_monad tactic.trace_state tactic.trace_state : tactic unit
+@monad.and_then.{1 1} unit unit tactic tactic.monad tactic.trace_state tactic.trace_state : tactic unit