diff --git a/tests/pkg/misc/Misc.lean b/tests/pkg/misc/Misc.lean
index fc3063b40f..24e0caf01a 100644
--- a/tests/pkg/misc/Misc.lean
+++ b/tests/pkg/misc/Misc.lean
@@ -10,3 +10,6 @@ open Lean Meta
   IO.println <| (← getEnv).getModuleIdxFor? ``foo
   IO.println <| (← getEnv).getModuleIdxFor? `auxDecl1
   IO.println "worked"
+
+set_option pp.all true
+#check f 10 10
diff --git a/tests/pkg/misc/Misc/Foo.lean b/tests/pkg/misc/Misc/Foo.lean
index 3389620db5..918d229608 100644
--- a/tests/pkg/misc/Misc/Foo.lean
+++ b/tests/pkg/misc/Misc/Foo.lean
@@ -11,3 +11,8 @@ def foo := 42
 local infix:50 " ≺ " => LE.le
 
 #check 1 ≺ 2
+
+local macro "my_refl" : tactic =>
+  `(tactic| rfl)
+
+def f (x y : Nat) (_h : x = y := by my_refl) := x