max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: check attribute name

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-03 18:15:55 -08:00
parent bc7455e04e
commit 2f3c6a8185
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Lean/Elab/Declaration.lean
View file

@ -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