test: macro scopes in Conv.congr (#1955)

leanprover · Dec 14, 2022 · 52d00e8 · 52d00e8
1 parent d5fb32a
commit 52d00e8
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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