Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-30 11:48 08e0e1d3

View on Github →

feat(category/traversable): instances for various collections (#217)

Estimated changes

Created category/traversable/equiv.lean

Modified data/array/lemmas.lean

added theorem array.to_list_of_heq

added def equiv.vector_equiv_array

added def equiv.vector_equiv_fin

Created data/buffer/basic.lean

added theorem buffer.append_list_mk_buffer

added theorem buffer.ext

added def buffer.list_equiv_buffer

added theorem buffer.to_list_append_list

Created data/dlist/instances.lean

added def dlist.list_equiv_dlist

Modified data/equiv/basic.lean

Created data/lazy_list2.lean

added def lazy_list.list_equiv_lazy_list

added def lazy_list.thunk.mk

Modified data/multiset.lean

Modified data/vector2.lean

deleted def equiv.vector_equiv_array

deleted def equiv.vector_equiv_fin

Modified logic/basic.lean

added theorem heq_of_eq_mp

Modified tactic/interactive.lean