Stream: general

Topic: nested namespaces

Reid Barton (Nov 05 2019 at 00:47):

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 (Nov 05 2019 at 00:50):

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 (Nov 05 2019 at 00:51):

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

Mario Carneiro (Nov 05 2019 at 01:23):

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 (Nov 05 2019 at 01:45):

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

Last updated: May 15 2021 at 23:13 UTC