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

chore: remove "local" before attribute command

Browse source 
`local` is now part of the `Term.attrInstance` parser.
This commit is contained in:
Leonardo de Moura 2020-12-05 07:47:28 -08:00
parent 9389bca624
commit 10102bf370
2 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -250,11 +250,10 @@ def elabMutual : CommandElab := fun stx => do
else
throwError "invalid mutual block"
/- parser! optional "local " >> "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "]" >> many1 ident -/
/- parser! "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "]" >> many1 ident -/
@[builtinCommandElab «attribute»] def elabAttr : CommandElab := fun stx => do
-- let persistent := stx[0].isNone -- TODO: remove
let attrs ← elabAttrs stx[3]
let idents := stx[5].getArgs
let attrs ← elabAttrs stx[2]
let idents := stx[4].getArgs
for ident in idents do withRef ident $ liftTermElabM none do
let declName ← resolveGlobalConstNoOverload ident.getId
Term.applyAttributes declName attrs

2
src/Lean/Parser/Command.lean
View file

@ -81,7 +81,7 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
@[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
@[builtinCommandParser] def «init_quot» := parser! "init_quot"
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "] " >> many1 ident
@[builtinCommandParser] def «attribute» := parser! "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "] " >> many1 ident
@[builtinCommandParser] def «export» := parser! "export " >> ident >> "(" >> many1 ident >> ")"
def openHiding := parser! atomic (ident >> "hiding") >> many1 ident
def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident