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

feat: add char (literal) as valid macro argument type

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 19:43:19 -08:00
parent 58b21fe0c9
commit 3b8e1f8591
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Parser/Syntax.lean
View file

@ -62,7 +62,7 @@ def identPrec := parser! ident >> optPrecedence
@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> many1Indent Term.matchAlt "'match' alternatives must be indented"
@[builtinCommandParser] def «syntax» := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> (ident >> optPrecedence)
def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> (ident >> optPrecedence)
def macroArgSimple := parser! ident >> ":" >> macroArgType
def macroArg := try strLitPrec <|> try macroArgSimple
def macroHead := try strLitPrec <|> try identPrec