From 36d508a4ce4520f05ddc7a5a8b28fa00a7676d1b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2020 08:11:19 -0800 Subject: [PATCH] feat: simplify `macroArg` --- src/Init/Lean/Parser/Syntax.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean index 6f5458cbf7..824f8f870e 100644 --- a/src/Init/Lean/Parser/Syntax.lean +++ b/src/Init/Lean/Parser/Syntax.lean @@ -59,7 +59,8 @@ def identPrec := parser! ident >> optional Syntax.precedence @[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 macroArg := parser! "(" >> optional (ident >> ":") >> syntaxParser >> ")" +def macroArgSimple := parser! ident >> ":" >> ident >> optional Syntax.precedence +def macroArg := try (strLitPrec <|> macroArgSimple) @[builtinCommandParser] def «macro» := parser! "macro " >> (strLitPrec <|> identPrec) >> many macroArg >> " : " >> ident >> unicodeSymbol "⇒" "=>" >> termParser end Command