Zulip Chat Archive

Stream: maths

Topic: topology predicate names

Patrick Massot (Jun 23 2020 at 16:25):

In a PR review, Sébastien wrote:

The usual classes are postfixed with space (like complete_space, compact_space, proper_space and so on), while the set versions are prefixed with is (like is_open, is_complete, is_compact and so on). Do you think it would be possible to adhere to this general convention also here (with separated_space and is_separated respectively)?

This is Sébastien's typical optimism. Actually the compactness predicate on sets is named compact. Should we try a general cleanup here? If people feel really brave we could even decide whether lemmas about closed sets contain closed or is_closed in their names.

Johan Commelin (Jun 23 2020 at 16:30):

I think such a general cleanup is a good idea.

Johan Commelin (Jun 23 2020 at 16:30):

Even better would be to fix the slight inconveniences in the script that Jason wrote for such renaming.

Johan Commelin (Jun 23 2020 at 16:30):

And then life will be easy

Kevin Buzzard (Jun 23 2020 at 16:31):

In another PR review Chris brought up a closely related question for the algebra hierarchy. Now might be a good time to come up with a global convention which we can stick to going forwards.

Sebastien Gouezel (Jun 23 2020 at 16:50):

Patrick Massot said:

This is Sébastien's typical optimism. Actually the compactness predicate on sets is named compact.

:rolling_on_the_floor_laughing:

Sebastien Gouezel (Jun 23 2020 at 16:52):

I would guess the is_... started because open is not allowed for CS reasons, so you need is_open, and then for uniformity you put is_ everywhere. I would be happy to get rid of is_ everywhere and rename open to CS_open and is_open to open.

Johan Commelin (Jun 23 2020 at 16:53):

How about open_namespace instead of CS_open :rolling_on_the_floor_laughing:

Sebastien Gouezel (Jun 23 2020 at 16:53):

I'm open to anything :)

Johan Commelin (Jun 23 2020 at 16:55):

We should choose something, so that this discussion/issue can finally be closed :)

Anatole Dedecker (Jun 23 2020 at 17:53):

Johan Commelin said:

How about open_namespace instead of CS_open :rolling_on_the_floor_laughing:

Another idea : why not have a specific notation for such reserved names ? Like we have # for... things with a # (I don't know the exact word). We could have something like : 

::import data.real.basic
::open nat
--Or even :
::lemma foo : ...

Adam Topaz (Jun 23 2020 at 17:58):

Even better would be: \ instead of :: (for the sake of LaTeX muscle memory).

Anatole Dedecker (Jun 23 2020 at 17:58):

Adam Topaz said:

Even better would be: \ instead of :: (for the sake of LaTeX muscle memory).

I thought about it, but it would mess up with VS-Code extension

Yury G. Kudryashov (Jun 23 2020 at 18:08):

I think that we shouldn't do changes like this without a migration plan for Lean 4.

Sebastien Gouezel (Jun 23 2020 at 18:22):

Lean 4 should allow us to have different meanings for open depending on the context, hopefully.

Kevin Buzzard (Jun 23 2020 at 18:23):

We tried that in maths -- we have 20 different meanings for normal. It just makes things more confusing :-/

Last updated: Dec 20 2023 at 11:08 UTC