Daniel Selsam (Apr 15 2021 at 03:36):
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 (Apr 15 2021 at 07:42):
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.
Last updated: May 07 2021 at 12:15 UTC