Zulip Chat Archive

@Mario Carneiro, now that you've finished with your norm_num port :-), could I get you to have a look at mathlib4#461, then mathlib4#457, then mathlib4#467 (they are sequentially dependent). These would be helpful for working on linarith!

Mario Carneiro (Oct 13 2022 at 06:14):

lol and I was hoping I could sleep

Scott Morrison (Oct 13 2022 at 06:15):

Definitely okay to do tomorrow :-)

Scott Morrison (Oct 13 2022 at 06:16):

I'm on a completely different timezone, but also about to stop for the day anyway. :-)

Mario Carneiro (Oct 13 2022 at 06:16):

uff, I'll do 457 tomorrow

Patrick Massot (Oct 13 2022 at 11:00):

Mario Carneiro said:

lol and I was hoping I could sleep

Young Mario would have never written this.

Kevin Buzzard (Oct 13 2022 at 11:02):

Does he have some kind of a _job_ now??

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib