Zulip Chat Archive

Stream: condensed mathematics

Topic: move me

Johan Commelin (Jul 20 2022 at 17:13):

If you want to help with cleaning up the project / restructuring it.

rg 'move me|move this' | wc -l
127

There's > 100 places where we temporarily dumped prereqs in the wrong file. Help with putting these in the right places (typically for_mathlib, or even directly to mathlib!) is very welcome.

Violeta Hernández (Jul 20 2022 at 18:37):

Here's a tiny contribution: #15574

Violeta Hernández (Jul 20 2022 at 18:37):

It's baffling this wasn't in mathlib already, it's literally the axiom of choice

Violeta Hernández (Jul 20 2022 at 18:38):

Is there any set theory stuff in there, by any chance? That's the sort of stuff I specialize with

Adam Topaz (Jul 20 2022 at 18:41):

Thanks @Violeta Hernández . Could you please add a comment in LTE where this is taken from mentioning the PR number?
This is an important point for anyone moving stuff to mathlib -- we should keep track in LTE of what's been moved.

Yaël Dillies (Jul 20 2022 at 23:30):

Violeta Hernández said:

Here's a tiny contribution: #15574

Wait, I literally have a PR for this.

Yaël Dillies (Jul 20 2022 at 23:36):

Yep: #14335

Johan Commelin (Jul 21 2022 at 06:02):

Whoops, I didn't realize that.

Yaël Dillies (Jul 21 2022 at 10:13):

My bad, I should have put a comment back in the code.

Last updated: Dec 20 2023 at 11:08 UTC