Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-23 18:01 fc7ac675

View on Github →

feat(data/string): add docstrings and improve semantics (#2497) Could have gone in #2493, but I didn't want to hold up #2478. Besides, what's a tiny pull request between friends. This "writing docstrings" thing really lets helps you discover tiny little tweaks here and here. <br> <br> <br>

Estimated changes