Zulip Chat Archive

Stream: mathlib4

Topic: !4#2778

Chris Hughes (Mar 10 2023 at 13:05):

I think that !4#2778 is worth celebrating because it was ported completely by start_port.sh, without any human changes needed.

Mario Carneiro (Mar 10 2023 at 13:06):

to be fair, it is an essentially small file

Jeremy Tan (Mar 11 2023 at 03:05):

!4#2797 should go about the same way

Jeremy Tan (Mar 25 2023 at 02:23):

And now !4#3091

Chris Hughes (Mar 25 2023 at 09:47):

Okay but !4#3091 doesn't contain a single declaration or do anything else. Maybe it should have been deleted when #9864 deleted the last useful code.

Yaël Dillies (Mar 25 2023 at 09:50):

#18653

Jeremy Tan (Apr 28 2023 at 06:14):

And now !4#3697

Last updated: Dec 20 2023 at 11:08 UTC