Zulip Chat Archive

Stream: mathlib4

Topic: Name for ZFC `Set`


Anatole Dedecker (Dec 25 2022 at 17:59):

I'd like to port SetTheory.Zfc.Basic (it's not high on the list, but it looks fun!). However, I'm not quite sure what to make about the fact that we can't use capitalization as a distinguising feature anymore. Should I make Set protected as ZFC.Set? Or Zfc.Set? Or no namespace and just ZFSet?
@Mario Carneiro @Violeta Hernández

Mario Carneiro (Dec 25 2022 at 18:00):

ZFSet sounds good to me

Mario Carneiro (Dec 25 2022 at 18:00):

It should be ZFC not Zfc when it shows up in filenames and types btw

Anatole Dedecker (Dec 25 2022 at 18:01):

Yes that's what I was going to ask, Zfc feels wrong to me, but I didn't want to break anything in Mathport

Reid Barton (Dec 25 2022 at 18:01):

I guess this file wants the ordinary Set way too often for ZFC.Set to be a good alternative

Anatole Dedecker (Dec 25 2022 at 18:02):

I would have made it protected, so it was more of a readability question between a dot and no dot

Anatole Dedecker (Dec 25 2022 at 18:10):

Type for docs#pSet.type is obviously not a valid identifier. Is it fine if I replace it by Index? I know I could use «Type» but it sounds a bit painful when Index seems clear enough to me.

Eric Wieser (Dec 25 2022 at 19:04):

Isn't dot notation enough to make s.Type legal syntax?

Eric Wieser (Dec 25 2022 at 19:05):

protected ZFC.Set seems sensible to me, especially if there's something else that would belong in that namespace

Yuyang Zhao (Dec 25 2022 at 19:15):

There would be ZFC.Class, and in the future, there will also be ZFC.Ordinal.

Eric Wieser (Dec 25 2022 at 19:22):

That seems pretty convincing to me

Anatole Dedecker (Dec 25 2022 at 19:50):

Eric Wieser said:

Isn't dot notation enough to make s.Type legal syntax?

Yes when used like that it works, but there are still a couple places where you need to write «Type»


Last updated: Dec 20 2023 at 11:08 UTC