Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
WIP: this month in mathlib (oct 2022)
I had some fun with @mcdoll's script in leanprover-community#48 (refactoring it and adding proper parsing of PR titles). It generated the following output. Feel free to copyedit and post. (I don't know if/when I'll have the time to do so.)
- Loading branch information