From 2fbcf4d681228bf2bb048d68869a183f5fc68dce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2020 18:14:06 -0800 Subject: [PATCH] chore: minor --- src/Init/Lean/Parser/Syntax.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean index 2b696bd064..171e79e03a 100644 --- a/src/Init/Lean/Parser/Syntax.lean +++ b/src/Init/Lean/Parser/Syntax.lean @@ -19,7 +19,7 @@ categoryParser `syntax rbp namespace Syntax def maxPrec := parser! nonReservedSymbol "max" true def precedenceLit : Parser := numLit <|> maxPrec -def «precedence» := parser! " : " >> precedenceLit +def «precedence» := parser! ":" >> precedenceLit @[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")" @[builtinSyntaxParser] def cat := parser! ident >> optional (try «precedence») @[builtinSyntaxParser] def atom := parser! strLit >> optional (try «precedence»)