Mathlib Changelog
v3
Changelog
About
Github
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