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

test: add trailing parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-15 16:17:39 -08:00
parent d9c6624a0a
commit d0f7467c95
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/macro2.lean
View file

@ -1,9 +1,14 @@
new_frontend
syntax term "+++":60 term:59 : term
syntax "<|" term "|>" : term
macro
| `(<| $x |>) => `($x + 1)
| `($a +++ $b) => `($a + $b + $b)
macro
| `(<| $x |>) => `($x +++ 1)
#check <| 2 |>