From 9736b8d79cb20cf0e5b60762811978ce606bfc55 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Dec 2015 11:17:42 -0800
Subject: [PATCH] test(tests/lean/attr_at3): add test for 'attribute ... at
 ...'

---
 tests/lean/attr_at3.lean              | 17 +++++++++++++++++
 tests/lean/attr_at3.lean.expected.out |  8 ++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 tests/lean/attr_at3.lean
 create mode 100644 tests/lean/attr_at3.lean.expected.out

diff --git a/tests/lean/attr_at3.lean b/tests/lean/attr_at3.lean
new file mode 100644
index 000000000..150fce778
--- /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 000000000..7805bcc88
--- /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