Zulip Chat Archive
Stream: mathlib4
Topic: !4#4888 IsAlgClosed
Johan Commelin (Jun 09 2023 at 10:38):
This PR has two annoying errors left. Help wanted. I will take a break for the moment.
Anne Baanen (Jun 09 2023 at 13:30):
Let me take a stab at these...
Anne Baanen (Jun 09 2023 at 15:32):
... and that's all I got time for! It should compile now, but the heartbeats are way too high.
Ruben Van de Velde (Jun 09 2023 at 15:35):
Not on CI, I'm afraid
Last updated: May 02 2025 at 03:31 UTC