From 3b6755dea1acf0a1a3196131dc3bf9cb7d1ea5c8 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 5 Nov 2019 13:37:58 -0800 Subject: [PATCH] doc: namespace A.B vs namespace A namespace B --- .../nested_namespace_vs_prefix.lean | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 tests/elabissues/nested_namespace_vs_prefix.lean diff --git a/tests/elabissues/nested_namespace_vs_prefix.lean b/tests/elabissues/nested_namespace_vs_prefix.lean new file mode 100644 index 0000000000..9e3c76ad14 --- /dev/null +++ b/tests/elabissues/nested_namespace_vs_prefix.lean @@ -0,0 +1,26 @@ +/- +@rwbarton found the following surprising: +-/ + +-- 1. When you are in `A.B`, you are not in `A`. + +def A.foo : String := "A.foo" + +namespace A.B + +def bar : String := foo -- error: unknown identifier 'foo' + +end A.B + +namespace A +namespace B + +def bar : String := foo -- succeeds + +end B +end A + +/- +I (@dselsam) agree it is a little weird, and suggest +either we disallow the first case or we make it sugar for the second. +-/