Zulip Chat Archive
Stream: mathlib4
Topic: Data.List.Range mathlib4#1463
Johan Commelin (Jan 10 2023 at 19:51):
I started this PR. I'll post here when I release my grip on the file.
Johan Commelin (Jan 10 2023 at 20:19):
There are a few errors left. But I'll take a break now.
Johan Commelin (Jan 10 2023 at 20:47):
should be error-free now
Last updated: May 02 2025 at 03:31 UTC