diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean
new file mode 100644
index 0000000000..36d1bd894b
--- /dev/null
+++ b/src/Lean/Elab/Attributes.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+import Lean.Parser.Basic
+import Lean.Attributes
+import Lean.MonadEnv
+
+namespace Lean
+namespace Elab
+
+structure Attribute :=
+(name : Name) (args : Syntax := Syntax.missing)
+
+instance Attribute.hasFormat : HasFormat Attribute :=
+⟨fun attr => Format.bracket "@[" (toString attr.name ++ (if attr.args.isMissing then "" else toString attr.args)) "]"⟩
+
+instance Attribute.inhabited : Inhabited Attribute := ⟨{ name := arbitrary _ }⟩
+
+def elabAttr {m} [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) : m Attribute := do
+-- rawIdent >> many attrArg
+let nameStx := stx.getArg 0;
+attrName ← match nameStx.isIdOrAtom? with
+  | none     => withRef nameStx $ throwError "identifier expected"
+  | some str => pure $ mkNameSimple str;
+env ← getEnv;
+unless (isAttribute env attrName) $
+  throwError ("unknown attribute [" ++ attrName ++ "]");
+let args := stx.getArg 1;
+-- the old frontend passes Syntax.missing for empty args, for reasons
+let args := if args.getNumArgs == 0 then Syntax.missing else args;
+pure { name := attrName, args := args }
+
+def elabAttrs {m} [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) : m (Array Attribute) :=
+(stx.getArg 1).foldSepArgsM
+  (fun stx attrs => do
+    attr ← elabAttr stx;
+    pure $ attrs.push attr)
+  #[]
+
+end Elab
+end Lean
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index d95ad33fc5..1ef377c9b8 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -4,19 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Elab.Command
+import Lean.Elab.Attributes
 
 namespace Lean
 namespace Elab
 namespace Command
 
-structure Attribute :=
-(name : Name) (args : Syntax := Syntax.missing)
-
-instance Attribute.hasFormat : HasFormat Attribute :=
-⟨fun attr => Format.bracket "@[" (toString attr.name ++ (if attr.args.isMissing then "" else toString attr.args)) "]"⟩
-
-instance Attribute.inhabited : Inhabited Attribute := ⟨{ name := arbitrary _ }⟩
-
 inductive Visibility
 | regular | «protected» | «private»
 
@@ -63,27 +56,6 @@ instance Modifiers.hasFormat : HasFormat Modifiers :=
 
 instance Modifiers.hasToString : HasToString Modifiers := ⟨toString ∘ format⟩
 
-def elabAttr {m} [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) : m Attribute := do
--- rawIdent >> many attrArg
-let nameStx := stx.getArg 0;
-attrName ← match nameStx.isIdOrAtom? with
-  | none     => withRef nameStx $ throwError "identifier expected"
-  | some str => pure $ mkNameSimple str;
-env ← getEnv;
-unless (isAttribute env attrName) $
-  throwError ("unknown attribute [" ++ attrName ++ "]");
-let args := stx.getArg 1;
--- the old frontend passes Syntax.missing for empty args, for reasons
-let args := if args.getNumArgs == 0 then Syntax.missing else args;
-pure { name := attrName, args := args }
-
-def elabAttrs {m} [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) : m (Array Attribute) :=
-(stx.getArg 1).foldSepArgsM
-  (fun stx attrs => do
-    attr ← elabAttr stx;
-    pure $ attrs.push attr)
-  #[]
-
 def elabModifiers (stx : Syntax) : CommandElabM Modifiers := do
 let docCommentStx := stx.getArg 0;
 let attrsStx      := stx.getArg 1;