Zulip Chat Archive
Stream: general
Topic: Pain
Kenny Lau (Oct 01 2018 at 08:25):
Patrick Massot (Oct 01 2018 at 08:28):
Is this part of your speedup effort?
Kenny Lau (Oct 01 2018 at 08:29):
it's already like that
Kenny Lau (Oct 01 2018 at 08:29):
I didn't change it
Patrick Massot (Oct 01 2018 at 08:29):
Not
Patrick Massot (Oct 01 2018 at 08:29):
https://github.com/leanprover/mathlib/blob/master/data/list/basic.lean#L100
Patrick Massot (Oct 01 2018 at 08:30):
Kenny, you're having personality splitting again
Kenny Lau (Oct 01 2018 at 08:31):
ah, it's L97
Last updated: Dec 20 2023 at 11:08 UTC