From fa938bb94c43d53b699e2f964be6daa181c4a061 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Dec 2015 11:50:08 -0800
Subject: [PATCH] feat(frontends/lean/decl_cmds): allow modifier to be provided
 after the 'attribute' keyword, test 'at' keyword

---
 library/algebra/group.lean       | 34 ++++++++++----------------------
 library/algebra/ring.lean        | 25 +++++++++--------------
 src/frontends/lean/decl_cmds.cpp | 12 ++++++++---
 3 files changed, 28 insertions(+), 43 deletions(-)

diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 0b9dbbe586..05154e4a9b 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -690,29 +690,15 @@ theorem neg_zero_helper [s : add_group A] (a : A) (H : a = 0) : - a = 0 :=
 
 end norm_num
 
-namespace simplifier
+attribute [simp]
+  algebra.zero_add algebra.add_zero algebra.one_mul algebra.mul_one
+  at simplifier.unit
 
-namespace unit
-attribute algebra.zero_add [simp]
-attribute algebra.add_zero [simp]
+attribute [simp]
+  algebra.neg_neg algebra.sub_eq_add_neg
+  at simplifier.neg
 
-attribute algebra.one_mul [simp]
-attribute algebra.mul_one [simp]
-end unit
-
-namespace neg
-attribute algebra.neg_neg [simp]
-attribute algebra.sub_eq_add_neg [simp]
-end neg
-
-namespace ac
-attribute algebra.add.assoc [simp]
-attribute algebra.add.comm [simp]
-attribute algebra.add.left_comm [simp]
-
-attribute algebra.mul.left_comm [simp]
-attribute algebra.mul.comm [simp]
-attribute algebra.mul.assoc [simp]
-end ac
-
-end simplifier
+attribute [simp]
+  algebra.add.assoc algebra.add.comm algebra.add.left_comm
+  algebra.mul.left_comm algebra.mul.comm algebra.mul.assoc
+  at simplifier.ac
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index ce8658e417..2ac0ad36b8 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -490,21 +490,14 @@ theorem pos_mul_neg_helper [s : ring A] (a b c : A) (H : a * b = c) : a * (-b) =
 
 end norm_num
 
-namespace simplifier
+attribute [simp]
+  algebra.zero_mul algebra.mul_zero
+  at simplifier.unit
 
-namespace unit
-attribute algebra.zero_mul [simp]
-attribute algebra.mul_zero [simp]
-end unit
+attribute [simp]
+  algebra.neg_mul_eq_neg_mul_symm algebra.mul_neg_eq_neg_mul_symm
+  at simplifier.neg
 
-namespace neg
-attribute algebra.neg_mul_eq_neg_mul_symm [simp]
-attribute algebra.mul_neg_eq_neg_mul_symm [simp]
-end neg
-
-namespace distrib
-attribute algebra.left_distrib [simp]
-attribute algebra.right_distrib [simp]
-end distrib
-
-end simplifier
+attribute [simp]
+  algebra.left_distrib algebra.right_distrib
+  at simplifier.distrib
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 738a26467b..67815078a0 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -1252,14 +1252,20 @@ static environment omit_cmd(parser & p) {
 
 static environment attribute_cmd_core(parser & p, bool persistent) {
     buffer<name> ds;
+    bool abbrev       = false;
+    decl_attributes attributes(abbrev, persistent);
+    bool parsed_attrs = false;
+    if (!p.curr_is_identifier()) {
+        attributes.parse(p);
+        parsed_attrs  = true;
+    }
     name d          = p.check_constant_next("invalid 'attribute' command, constant expected");
     ds.push_back(d);
     while (p.curr_is_identifier()) {
         ds.push_back(p.check_constant_next("invalid 'attribute' command, constant expected"));
     }
-    bool abbrev     = false;
-    decl_attributes attributes(abbrev, persistent);
-    attributes.parse(p);
+    if (!parsed_attrs)
+        attributes.parse(p);
     name ns = get_namespace(p.env());
     if (p.curr_is_token(get_at_tk())) {
         if (!persistent)