Zulip Chat Archive
Stream: mathlib4
Topic: !4#2931
Jeremy Tan (Mar 16 2023 at 14:10):
!4#2931 I pondered about how to solve the last few errors here, but to no avail. Can somebody help please?
Adam Topaz (Mar 16 2023 at 14:30):
I fixed all the errors in this branch
Adam Topaz (Mar 16 2023 at 14:30):
But I didn't do any of the linting, etc.
Jeremy Tan (Mar 16 2023 at 14:32):
Should probably lint pass since the file is pretty short. (But you never know...)
Jeremy Tan (Mar 16 2023 at 14:34):
wait
Jeremy Tan (Mar 16 2023 at 17:04):
all done, can be merged now
Last updated: Dec 20 2023 at 11:08 UTC