diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean index 17e38995ed..cf9a50ffa4 100644 --- a/src/Init/Lean/Parser/Syntax.lean +++ b/src/Init/Lean/Parser/Syntax.lean @@ -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