mathlib:namespace

Stream: lean4

[Daniel Selsam]

Mario Carneiro said:

I don't want to add an extra 8 characters on a substantial number of fully qualified names in usual mathlib proofs

I agree that is a significant downside. I just created an issue for it https://github.com/dselsam/mathport/issues/25 Maybe it isn't a good idea to put everything in a namespace, but it just seems like bad style to put things in _root_. For example, you may break if lean4 adds a definition. Also, you can't hide names when importing. Signing off now but to be continued. Thanks for your help tonight.

[Gabriel Ebner]

We've had the same discussion in Lean 3, and I don't think anything has changed in Lean 4 that would change the outcome of this discussion.

For example, you may break if lean4 adds a definition.

All changes in core cause breakage, and name collisions are the easiest to fix. So this is not a big win.