Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-11 10:07 4e3b89c3

View on Github →

feat(tactic/ext): make the attribute incremental

Estimated changes

Modified category_theory/isomorphism.lean

Created core/data/list.lean

added def list.partition_map

Created core/default.lean

Modified data/list/basic.lean

modified theorem list.erase_diff_erase_sublist_of_sublist

modified theorem list.index_of_eq_length

Modified data/sum.lean

added def sum.map

Modified docs/tactics.md

Modified tactic/ext.lean

added def ext_param_type

Modified tactic/pi_instances.lean