Std4 vs Mathlib4

Stream: mathlib4

[Adam Topaz]

Do we have some way of telling (e.g. using the port_status script) which files are intended to be ported into mathlib4 and which ones will be part of Std4? E.g. I imagine that control.applicative, data.string.basic and such things will likely go to Std4.

[Ruben Van de Velde]

I think we've been porting those things into mathlib4 and then Mario comes along and moves them

[Adam Topaz]

:rofl: okay

[Adam Topaz]

@Mario Carneiro can you confirm that this is your intended workflow? ;)

[Mario Carneiro]

Yes. Note that files aren't really "moved" to std4, rather most of their content is reproduced and the mathlib4 file becomes a collection of #aligns and alias commands