nested namespaces

Stream: general

[Reid Barton]

I found out today that

namespace A.B
...
end A.B

is not entirely equivalent to

namespace A
namespace B
...
end B
end A

[Reid Barton]

If you're in a namespace C and you refer to a name x and C.x exists, then Lean will assume you mean C.x and not consider any other potential x. For this purpose, the latter sequence above is "in" both namespaces A and A.B (I assume A.B gets checked first, though I didn't test), while the former sequence is only "in" namespace A.B, not namespace A.

[Reid Barton]

If you're writing category theory modules, I recommend not writing namespace category_theory.foo (as I used to).

[Mario Carneiro]

namespace A.B can be seen as having two effects: Making all new definitions x land as A.B.x, and opening the namespace A.B so that A.B.foo is accessible. If you use nested namespace, the former effect (the target namespace) is the same, but you have two opens instead of one. (A namespace is also something like a high-priority open; it will always trump any other open when there is a conflict, while a conflict between two opens results in an ambiguity error.)

[Reid Barton]

I find it really weird. You're in some particular namespace at any given point, it shouldn't matter how you got there.