Zulip Chat Archive

Stream: general

Topic: nat.mul_le_mul


view this post on Zulip Kevin Buzzard (Jun 29 2020 at 10:08):

Is it intentional that nat.mul_le_mul asks twice for proofs that 0 <= (n : nat)? Is this for some general consistency with mul_le_mul lemmas? I thought the whole point of namespaced lemmas like that was precisely so you could change the inputs appropriately.

view this post on Zulip Johan Commelin (Jun 29 2020 at 10:09):

I guess it is not.

view this post on Zulip Johan Commelin (Jun 29 2020 at 10:10):

Probably an artifact from me reproving a bunch of lemmas specifically for nat when ripping algebra out of core.

view this post on Zulip Johan Commelin (Jun 29 2020 at 10:10):

I guess this is in core?

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 10:10):

Yep: src#nat.mul_le_mul

view this post on Zulip Johan Commelin (Jun 29 2020 at 10:12):

Surrounding lemmas have the same problem.

view this post on Zulip Johan Commelin (Jun 29 2020 at 10:19):

I'm trying to fix this, but lean spits out loads of unrelated errors...

view this post on Zulip Johan Commelin (Jun 29 2020 at 10:20):

Is github down for everyone or just me?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 10:20):

maybe everyone?

view this post on Zulip Shing Tak Lam (Jun 29 2020 at 10:21):

https://www.githubstatus.com/

Everyone

view this post on Zulip Johan Commelin (Jun 29 2020 at 10:21):

Stupid github

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 10:21):

back now but slow

view this post on Zulip Johan Commelin (Jun 29 2020 at 10:23):

https://github.com/leanprover-community/lean/compare/fix-nat-lemmas?expand=1


Last updated: May 16 2021 at 20:13 UTC