Zulip Chat Archive

Stream: std4

Topic: What lemmas do (not) belong to std?


Yury G. Kudryashov (Jan 18 2023 at 05:16):

I understand that a definition/structure belongs to std if it's useful for programmers or is a dependency of a definition that is useful for programmers. What about lemmas? What stays in mathlib, what goes to std?

Yury G. Kudryashov (Jan 18 2023 at 05:17):

E.g., should most of lemmas about Lists that don't need [Group] etc go to std or not?

James Gallicchio (Jan 18 2023 at 05:36):

Can't speak for Mario but I think the standard so far has just been "does this not require mathlib stuff?" (so probably most lemmas about List should go in std)

James Gallicchio (Jan 18 2023 at 05:37):

e.g. I'm working on moving List.Perm to Std since it's useful for programmers and most of the lemmas don't depend on mathlib stuff

Mario Carneiro (Jan 18 2023 at 07:52):

Yes, James is right. Things that require too much of mathlib are out, but "is a dependency of a definition that is useful for programmers" can be interpreted broadly to include lemmas about existing structures that could potentially be useful for downstream programming tasks. As a result, I anticipate almost everything in mathlib's Data.List to move to std eventually, although I am waiting until all the porting work settles down to do that


Last updated: Dec 20 2023 at 11:08 UTC