Zulip Chat Archive
Stream: general
Topic: protected
Johan Commelin (May 23 2019 at 09:21):
Is there any way in which we can make topological_space.is_open protected?
Johan Commelin (May 23 2019 at 09:21):
As soon as you namespace topological_space you need to _root_.is_open all the time.
Mario Carneiro (May 23 2019 at 09:26):
no, but we could rename it to is_open'
Johan Commelin (May 23 2019 at 09:27):
It would be nice if protected was an attribute that you could locally set or remove.
Johan Commelin (May 23 2019 at 09:28):
@Sebastian Ullrich Will Lean 4 make this possible?
Sebastian Ullrich (May 23 2019 at 10:28):
It probably should. If there's no reason against some metadata not being an attribute, it should become one.
Keeley Hoek (May 23 2019 at 10:43):
Even if there was a problem, a manual @[hidden] would be lovely
Last updated: Dec 20 2023 at 11:08 UTC