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