diff --git a/tests/lean/run/macro2.lean b/tests/lean/run/macro2.lean index 519b1cd15a..d315a7a4ba 100644 --- a/tests/lean/run/macro2.lean +++ b/tests/lean/run/macro2.lean @@ -21,4 +21,6 @@ macro_rules #check <| ~2 |> +#check <| ~~2 |> + #check <| <| 3 |> |>