Zulip Chat Archive

Stream: mathlib4

Topic: mathlib4 vs std4


David Renshaw (Sep 19 2022 at 17:08):

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 (Sep 22 2022 at 17:58):

@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 (Sep 22 2022 at 18:00):

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.


Last updated: Dec 20 2023 at 11:08 UTC