chore(init/data/set): Delete

[YaelDillies]

To be (obviously!) restored on the mathlib side. Followup to #675

[fpvandoorn]

Feel free to move the rest to mathlib as well. Except for set_of because that's referenced by Lean.

Should we leave set_of here?

[YaelDillies]

Oh, I missed this. Where is it referenced?

[fpvandoorn]

Probably in the C++ code, on how to parse { ... | ... }.

[fpvandoorn]

Then again, I don't think it causes any problems if we move this to mathlib, except that you'll get an error when writing { ... | ... } before you import the appropriate file. But I'd like to let @gebner chime in on that.

[gebner]

I believe set_of is the only reason some of the set definition is still in core (see https://github.com/leanprover-community/lean/pull/675#issuecomment-1024411237). There's also a test that checks whether every definition referenced from the C++ side actually exists in the library: bors try

[bors[bot]]

try

Build failed:

• Build linux Debug

[fpvandoorn]

Relevant line in the build failure: init.data.basic cannot find init.data.set.

[eric-wieser]

bors try

[bors[bot]]

try

Build failed:

• Build linux Release

[eric-wieser]

Looks like there are 24 failing tests (search for ***Failed in the logs to find them)