doc: namespace A.B vs namespace A namespace 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.
+-/