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»)