ZFA namespace

Stream: general

[Yury G. Kudryashov]

Should we move ZFA stuff in a namespace? Someone who imports all of mathlib can confuse, e.g., docs#finsets with docs#finset. Also, moving to a NS will allow us to use ZFA.finset instead of finsets.

[Mario Carneiro]

no it's not supposed to be finset

[Mario Carneiro]

it is hereditary finsets

[Yury G. Kudryashov]

Also, the module docstring should give some background about ZFA.

[Mario Carneiro]

in fact ZFA is also a bit of a misnomer because ZFA has infinite stuff

[Yury G. Kudryashov]

I don't see why the name finsets is better than finset. hfinset?

[Mario Carneiro]

this is more like "grade school set theory"

[Mario Carneiro]

where you write down examples of sets like {{}, 3, {14}}

[Yury G. Kudryashov]

It would be nice to have some references in the module docstring and an explanation of what happens here.

[Yury G. Kudryashov]

And I think that hiding a rarely used theory in a namespace is a good idea.

[Mario Carneiro]

ok, but ZFA makes it sound scarier than it should be

[Mario Carneiro]

the main purpose is to be able to do computable set theory toy examples

[Yury G. Kudryashov]

What NS would you suggest?

[Yury G. Kudryashov]

The only reason I opened this file was to forward-port a change to the module docstring. Probably, I will never open it in the next year or ten.

[Mario Carneiro]

ok, so maybe just leave it?

[Mario Carneiro]

It's a leaf file anyway

[Yury G. Kudryashov]

My main concern is that someone imports the whole Mathlib, then accidentally writes Finsets α instead of Finset α.

[Mario Carneiro]

Maybe put a warning in the docstring?

[Mario Carneiro]

That's going to be an issue no matter what it is called

[Yury G. Kudryashov]

If it's in a namespace, then code completion won't suggest it after you type Finse

[Mario Carneiro]

it should, that's definitely a lean 4 bug (lean 3 would do so)

[Yury G. Kudryashov]

Probably, it's not a Lean 4 bug but my wrong guess.

[Mario Carneiro]

plus it shows up in searches and such

[Yury G. Kudryashov]

I didn't test.

[Mario Carneiro]

as long as it has a name vaguely related to finset we will need to address the difference in the docstring