From 52d00e8944f5afc8fa1b4066ae30065a8682eb82 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 14 Dec 2022 17:43:26 +0100 Subject: [PATCH] test: macro scopes in Conv.congr (#1955) --- tests/lean/conv1.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/lean/conv1.lean b/tests/lean/conv1.lean index 55667aa56aaa..d90a9575d9be 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