From ac2fb7e149b4e1bfea06e1fe215377789b24e77b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 18 Jan 2020 19:19:18 -0800
Subject: [PATCH] feat: allow `ident`, `num` (numeric literals) and `str`
 (string literals) as macro argument types

---
 src/Init/Lean/Parser/Syntax.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean
index 80546545e1..17e38995ed 100644
--- a/src/Init/Lean/Parser/Syntax.lean
+++ b/src/Init/Lean/Parser/Syntax.lean
@@ -62,8 +62,9 @@ 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 macroArgSimple := parser! ident >> ":" >> ident >> optPrecedence
-def macroArg := try strLitPrec <|> try macroArgSimple
+def macroArgType   := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> (ident >> optPrecedence)
+def macroArgSimple := parser! ident >> ":" >> macroArgType
+def macroArg  := try strLitPrec <|> try macroArgSimple
 def macroHead := try strLitPrec <|> try identPrec
 def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")"
 def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"