From 2f3c6a8185c1c2253172578fce528bbfcc92ee09 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 3 Jan 2020 18:15:55 -0800
Subject: [PATCH] feat: check attribute name

---
 src/Init/Lean/Elab/Declaration.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/Elab/Declaration.lean b/src/Init/Lean/Elab/Declaration.lean
index f5cf88427e..bc61bed227 100644
--- a/src/Init/Lean/Elab/Declaration.lean
+++ b/src/Init/Lean/Elab/Declaration.lean
@@ -76,13 +76,14 @@ match stx with
 def elabAttr (stx : Syntax) : CommandElabM Attribute := do
 -- rawIdent >> many attrArg
 let nameStx := stx.getArg 0;
-name ← match nameStx.isIdOrAtom? with
+attrName ← match nameStx.isIdOrAtom? with
   | none     => throwError nameStx "identifier expected"
   | some str => pure $ mkNameSimple str;
--- TODO: check whether it is valid attribute or not
+unlessM (liftIO stx (isAttribute attrName)) $
+  throwError stx ("unknown attribute [" ++ attrName ++ "]");
 let argStxs := (stx.getArg 1).getArgs;
 args ← argStxs.mapM elabAttrArg;
-pure { name := name, args := args }
+pure { name := attrName, args := args }
 
 def elabAttrs (stx : Syntax) : CommandElabM (Array Attribute) :=
 (stx.getArg 1).foldSepArgsM