Zulip Chat Archive

Stream: new members

Topic: Removed from mathlib


view this post on Zulip Pedro Minicz (Oct 23 2020 at 00:21):

How often do lemmas get removed from mathlib, if at all?

view this post on Zulip Pedro Minicz (Oct 23 2020 at 00:22):

(Asking because I can swear two_pos : (0 : ℕ) < 2 used to exist.)

view this post on Zulip Bryan Gin-ge Chen (Oct 23 2020 at 00:22):

Generally we only remove redundant lemmas; not sure how often that is though, maybe a few times a week?

view this post on Zulip Reid Barton (Oct 23 2020 at 00:23):

See #4295

view this post on Zulip Reid Barton (Oct 23 2020 at 00:24):

(How to find it: git log -S two_pos)

view this post on Zulip Bryan Gin-ge Chen (Oct 23 2020 at 00:24):

You can also find it by searching the mathlib github repo for two_pos.

view this post on Zulip Pedro Minicz (Oct 23 2020 at 00:29):

Reid Barton said:

(How to find it: git log -S two_pos)

Cool. Always good to learn more git!

view this post on Zulip Mario Carneiro (Oct 23 2020 at 05:40):

Hm, I don't approve of removing lemmas just because they are duplicates, especially if they are explicitly aliases

view this post on Zulip Bryan Gin-ge Chen (Oct 23 2020 at 05:43):

It doesn't seem to me like they were explicitly aliases in this case though.

view this post on Zulip Mario Carneiro (Oct 23 2020 at 05:47):

I think we should be using the alias command a lot more than we do; names are hard and our naming system is not completely unambiguous

view this post on Zulip Mario Carneiro (Oct 23 2020 at 05:48):

in this case I think there is a clear argument for zero_lt_two and two_pos being aliases

view this post on Zulip Scott Morrison (Oct 23 2020 at 08:37):

Sorry, this was me. Point taken.


Last updated: May 16 2021 at 20:13 UTC