mathlib4 vs std4

Stream: mathlib4

[David Renshaw]

For a given mathlib3 item, how do we decide whether it belongs in mathlib4 or in std4?

For example, where should stuff from data/list/pairwise live?

What about the remaining unported lemmas from logic/basic? Do they all go in Std/Logic.lean?

[David Renshaw]

@Mario Carneiro answered this in today's mentoring meeting. There should still be a one-to-one mapping of files from mathlib3 into mathlib4, but some of the files will thinned out as their definitions move to std4.

[David Renshaw]

We can imagine two separate processes:

1. items from mathlib3 get ported to mathlib4
2. some items from mathlib4 get pulled up into std4

There does not need to be tight coordination between these processes.