From e488c0f3dc9a9b2beeef62ea4bc5c74cd1adc6f5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2020 18:03:50 -0800 Subject: [PATCH] fix: missing `try` --- src/Init/Lean/Parser/Syntax.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean index 2349b12227..4207db43cf 100644 --- a/src/Init/Lean/Parser/Syntax.lean +++ b/src/Init/Lean/Parser/Syntax.lean @@ -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"