diff --git a/tests/lean/run/macro2.lean b/tests/lean/run/macro2.lean index 24e7cd1766..1af08ae5ae 100644 --- a/tests/lean/run/macro2.lean +++ b/tests/lean/run/macro2.lean @@ -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 |>