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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-10 16:43:44 -07:00
parent f838b80e03
commit f92166e913
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/termParserAttr.lean
View file

@ -16,7 +16,7 @@ open Lean.Parser
@[termParser] def tst := parser! "(|" >> termParser >> optional (symbol ", " >> termParser) >> "|)"
@[termParser] def boo : ParserDescr :=
ParserDescr.node `boo
ParserDescr.node `boo 10
(ParserDescr.andthen
(ParserDescr.symbol "[|")
(ParserDescr.andthen