Zulip Chat Archive

Stream: general

Topic: lean core vs mathlib

Kenny Lau (May 10 2020 at 05:40):

What is the criterion for a definition / theorem to be put in mathlib vs in lean core?

Kevin Buzzard (May 10 2020 at 06:33):

Does it have to be in core if it's needed to make the core unit tests work?

Mario Carneiro (May 10 2020 at 06:39):

well yes, although you could remove the tests

Kevin Buzzard (May 10 2020 at 06:42):

You once told me that this was like breaking the code and then covering your tracks

Last updated: Aug 03 2023 at 10:10 UTC