Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-07 18:09 4e8427ec

View on Github →

fix(data/list/defs): remove map_head; rename map_last to modify_last (#4507) map_head is removed in favour of the equivalent modify_head. map_last is renamed to modify_last for consistency with the other modify_* functions.

Estimated changes