Zulip Chat Archive

Stream: maths

Topic: topology predicate names


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 23 2020 at 16:30):

I think such a general cleanup is a good idea.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 23 2020 at 16:30):

And then life will be easy

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 23 2020 at 16:53):

How about open_namespace instead of CS_open :rolling_on_the_floor_laughing:

view this post on Zulip Sebastien Gouezel (Jun 23 2020 at 16:53):

I'm open to anything :)

view this post on Zulip Johan Commelin (Jun 23 2020 at 16:55):

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

view this post on Zulip 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 : ...

view this post on Zulip Adam Topaz (Jun 23 2020 at 17:58):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Jun 23 2020 at 18:22):

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

view this post on Zulip 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: May 09 2021 at 11:09 UTC