revisiting qualified imports

Stream: lean4

[Calvin Lee]

There is a thread from a few years back (#lean4 > ✔ qualified imports?) about how qualified imports were not possible in Lean4.
I'm curious if anything has changed here, or if core maintainers would be OK with it in the language. Specifically, since we have so much more code in Lean4 now with mathlib, it's a bit hard to manage _root_ qualified names.

For example, I'm currently working with the krull dimension docs4#height, which does not live under a namespace. This means that whenever I want to create another notion of height, it must be both qualifed, and refer to the Krull height as _root_.height to avoid conflicts.

[Kyle Miller]

How is this other notion of height defined? Could you define it protected so that it must be referred to in a qualified way, freeing up height for the root one?

[Calvin Lee]

Yes, I was planning on making these each qualified under a certain type (e.g. Ideal.height, Ring.height, etc)
protected seems to work! I think this is what I was looking for

[Scott Morrison]

I think we also shouldn't be afraid to namespace existing definitions.

[Scott Morrison]

CategoryTheory is essentially all in its own namespace, largely by historical accident (I PR'd a bunch before realising that wasn't the standard thing to do?), and I don't think that has particularly hurt.