Zulip Chat Archive
Stream: mathlib4
Topic: rintro?
Patrick Massot (Oct 20 2023 at 22:06):
Is rintro? still missing?
Scott Morrison (Oct 21 2023 at 03:19):
Yes.
Last updated: May 02 2025 at 03:31 UTC
Is rintro? still missing?
Yes.
Last updated: May 02 2025 at 03:31 UTC