From acba8d4a4ae0626ca746b1d10ee960e646f185ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Dec 2020 16:01:52 -0800 Subject: [PATCH] chore: cleanup --- src/Lean/Parser/Syntax.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 229bc50c3d..e59d54c4d3 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -30,8 +30,6 @@ builtin_initialize @[inline] def syntaxParser (rbp : Nat := 0) : Parser := categoryParser `stx rbp --- TODO: `max` is a bad precedence name. Find a new one. -def maxSymbol := parser! nonReservedSymbol "max" true def «precedence» := parser! ":" >> precedenceParser maxPrec def optPrecedence := optional (atomic «precedence») @@ -39,7 +37,7 @@ namespace Syntax @[builtinPrecParser] def numPrec := checkPrec maxPrec >> numLit @[builtinPrioParser] def numPrio := checkPrec maxPrec >> numLit -@[builtinPrioParser] def highPrio := parser!:maxPrec nonReservedSymbol "high" true +@[builtinPrioParser] def highPrio := parser!:maxPrec nonReservedSymbol "high" @[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")" @[builtinSyntaxParser] def cat := parser! ident >> optPrecedence