Zulip Chat Archive
Stream: std4
Topic: Jannis' PRs
Gabriel Ebner (Jan 09 2023 at 23:52):
@Mario Carneiro We have a a lot of PRs from Jannis. From what I gather, this is mostly utility code from Aesop. This is starting to block mathlib4#1364. Is there anything that you're waiting for here?
Last updated: Dec 20 2023 at 11:08 UTC