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. +-/