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

chore(library/init/lean/parser/command): simple open command syntax

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-17 14:33:33 -07:00
parent 18d47a2b74
commit 611635281b
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/init/lean/parser/command.lean
View file

@ -85,11 +85,12 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (symbolOrIdent "true" <|> symbolOrIdent "false" <|> strLit <|> numLit)
@[builtinCommandParser] def «attribute» := parser! optional "local " >> "attribute " >> "[" >> sepBy1 attrInstance ", " >> "]" >> many1 ident
@[builtinCommandParser] def «export» := parser! "export " >> ident >> "(" >> many1 ident >> ")"
def openOnly := parser! try ("(" >> ident) >> many ident >> ")"
def openHiding := parser! try ("(" >> "hiding") >> many1 ident >> ")"
def openHiding := parser! try (ident >> "hiding") >> many1 ident
def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident
def openRenaming := parser! try ("(" >> "renaming") >> sepBy1 openRenamingItem ", " >> ")"
@[builtinCommandParser] def «open» := parser! "open " >> many1 ident >> optional openOnly >> optional openRenaming >> optional openHiding
def openRenaming := parser! try (ident >> "renaming") >> sepBy1 openRenamingItem ", "
def openOnly := parser! try (ident >> "(") >> many1 ident >> ")"
def openSimple := parser! many1 ident
@[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple)
/- Lean3 command declaration commands -/
def maxPrec := parser! symbolOrIdent "max"