Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-06 10:22 6b59725c

View on Github →

chore(control/traversable/{basic,equiv,instances,lemmas}): linting (#4444) The nolints in instances.lean are there because all the arguments need to be there for is_lawful_traversable. In the same file, I moved traverse_map because it does not need the is_lawful_applicative instances.

Estimated changes