diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean
index 55667aa56a..d90a9575d9 100644
--- a/tests/lean/conv1.lean
+++ b/tests/lean/conv1.lean
@@ -242,3 +242,6 @@ example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 5) _
 example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 2 5) _ + _
 example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 1 5) _ + _
 example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 1 2 5) _ + _
+
+macro "bla" : term => `(?a)
+example : 1 = 1 := by conv => apply bla; congr