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

fix: missing try

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-15 18:03:50 -08:00
parent 148b92e9ea
commit e488c0f3dc
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -21,8 +21,8 @@ def maxPrec := parser! nonReservedSymbol "max"
def precedenceLit : Parser := numLit <|> maxPrec
def «precedence» := parser! " : " >> precedenceLit
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat := parser! ident >> optional «precedence»
@[builtinSyntaxParser] def atom := parser! strLit >> optional «precedence»
@[builtinSyntaxParser] def cat := parser! ident >> optional (try «precedence»)
@[builtinSyntaxParser] def atom := parser! strLit >> optional (try «precedence»)
@[builtinSyntaxParser] def num := parser! nonReservedSymbol "num"
@[builtinSyntaxParser] def str := parser! nonReservedSymbol "str"
@[builtinSyntaxParser] def char := parser! nonReservedSymbol "char"