max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-14 16:01:52 -08:00
parent 6909faf4a2
commit acba8d4a4a
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Parser/Syntax.lean
View file

@ -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