What lemmas do (not) belong to std?

Stream: std4

[Yury G. Kudryashov]

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]

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

[James Gallicchio]

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]

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]

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