From e0897ae78c1a3582bc17c0bc347268059165a0ae Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Fri, 30 Jul 2021 13:46:27 -0700
Subject: [PATCH] chore: test unexpanders inside namespaces

---
 tests/lean/unexpandersNamespaces.lean              | 11 +++++++++++
 tests/lean/unexpandersNamespaces.lean.expected.out |  2 ++
 2 files changed, 13 insertions(+)
 create mode 100644 tests/lean/unexpandersNamespaces.lean
 create mode 100644 tests/lean/unexpandersNamespaces.lean.expected.out

diff --git a/tests/lean/unexpandersNamespaces.lean b/tests/lean/unexpandersNamespaces.lean
new file mode 100644
index 0000000000..14e23a23aa
--- /dev/null
+++ b/tests/lean/unexpandersNamespaces.lean
@@ -0,0 +1,11 @@
+namespace Foo
+
+abbrev List (α : Type u) : Type := Unit
+
+def List.nil {α : Type u} : List α := ()
+def List.cons {α : Type u} (x : α) (xs : List α) : List α := ()
+
+#check @List.nil Unit
+#check @_root_.List.nil Unit
+
+end Foo
diff --git a/tests/lean/unexpandersNamespaces.lean.expected.out b/tests/lean/unexpandersNamespaces.lean.expected.out
new file mode 100644
index 0000000000..2bc0ff6bd1
--- /dev/null
+++ b/tests/lean/unexpandersNamespaces.lean.expected.out
@@ -0,0 +1,2 @@
+List.nil : List Unit
+[] : _root_.List Unit