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

chore: use try to fix : overload

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-14 14:19:44 -08:00
parent 2e668d9052
commit abc6bc1447
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

@ -22,8 +22,8 @@ categoryParser `syntax rbp
namespace Syntax
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat := parser! ident >> optional (":" >> numLit)
@[builtinSyntaxParser] def atom := parser! strLit >> optional (":" >> numLit)
@[builtinSyntaxParser] def cat := parser! ident >> optional (try (":" >> numLit))
@[builtinSyntaxParser] def atom := parser! strLit >> optional (try (":" >> numLit))
@[builtinSyntaxParser] def num := parser! nonReservedSymbol "num"
@[builtinSyntaxParser] def str := parser! nonReservedSymbol "str"
@[builtinSyntaxParser] def char := parser! nonReservedSymbol "char"