diff --git a/tests/lean/attr_at3.lean b/tests/lean/attr_at3.lean
new file mode 100644
index 0000000000..150fce778e
--- /dev/null
+++ b/tests/lean/attr_at3.lean
@@ -0,0 +1,17 @@
+namespace bla
+definition f (a : nat) := a + 1
+attribute f [reducible] at foo
+print f
+end bla
+
+
+section
+  open foo
+  print bla.f
+end
+
+print bla.f
+
+namespace foo
+  print bla.f
+end foo
diff --git a/tests/lean/attr_at3.lean.expected.out b/tests/lean/attr_at3.lean.expected.out
new file mode 100644
index 0000000000..7805bcc883
--- /dev/null
+++ b/tests/lean/attr_at3.lean.expected.out
@@ -0,0 +1,8 @@
+definition bla.f : ℕ → ℕ :=
+λ (a : ℕ), a + 1
+definition bla.f [reducible] : ℕ → ℕ :=
+λ (a : ℕ), a + 1
+definition bla.f : ℕ → ℕ :=
+λ (a : ℕ), a + 1
+definition bla.f [reducible] : ℕ → ℕ :=
+λ (a : ℕ), a + 1