lean4-htt/tests
Leonardo de Moura 3e028e3812 feat: allow syntax command to use existing parser declarations
@Kha Note that I had to change the pattern. After I replaced,
```
syntax text : child
```
with
```
syntax Prelim.text  : child
```
Thus, I wrote
```
`(child|$t:text)
```
as
```
`(child|$t)
```
It works for this example, but it may be a problem in general.
2020-06-16 15:08:23 -07:00
..
bench chore: delete unused file 2020-06-16 10:41:42 -07:00
compiler chore: simplify checkPrec 2020-06-10 14:34:58 -07:00
elabissues chore: fix syntax 2020-05-21 09:57:35 -07:00
ir chore(tests): fix do syntax in tests 2019-06-30 13:04:34 +02:00
lean feat: add ParserDescr.parser constructor for embedding parser definitions into parser descriptions 2020-06-16 14:06:46 -07:00
playground feat: allow syntax command to use existing parser declarations 2020-06-16 15:08:23 -07:00
plugin chore: fix tests 2020-05-26 15:05:01 -07:00
.gitignore chore: move bin/ and .oleans into build directory 2020-05-14 14:47:54 +02:00
common.sh chore: add comment 2020-05-15 11:26:24 -07:00