Zulip Chat Archive
Stream: mathlib4
Topic: Old PRs
Jeremy Tan (Mar 17 2023 at 09:27):
This thread is for reviewing old porting PRs (that are either all fixed up or otherwise), such as
Notification Bot (Mar 17 2023 at 09:37):
A message was moved here from #mathlib4 > ##18596 by Jeremy Tan.
Jeremy Tan (Mar 19 2023 at 16:35):
!4#2905 is ready to merge (again)
Last updated: May 02 2025 at 03:31 UTC