Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-11-07 06:09
4ae6a578
View on Github →
fix(data/array): update to lean
Estimated changes
Modified
data/array/lemmas.lean
added
theorem
array.mem.def
deleted
theorem
array.mem_iff_list_mem
deleted
theorem
array.mem_iff_rev_list_mem
deleted
theorem
array.mem_iff_rev_list_mem_core
added
theorem
array.mem_rev_list
added
theorem
array.mem_rev_list_core
added
theorem
array.mem_to_list
added
theorem
array.mem_to_list_enum
modified
theorem
array.push_back_rev_list
modified
theorem
array.push_back_rev_list_core
modified
theorem
array.push_back_to_list
added
theorem
array.read_foreach
deleted
def
array.read_foreach
added
theorem
array.read_foreach_aux
deleted
def
array.read_foreach_aux
added
theorem
array.read_map
deleted
def
array.read_map
added
theorem
array.read_map₂
deleted
def
array.read_map₂
deleted
theorem
array.read_write
deleted
theorem
array.read_write_eq
deleted
theorem
array.read_write_ne
added
theorem
array.rev_list_foldr
added
theorem
array.rev_list_foldr_aux
modified
theorem
array.rev_list_length
modified
theorem
array.rev_list_length_aux
modified
theorem
array.rev_list_reverse
modified
theorem
array.rev_list_reverse_core
added
theorem
array.to_list_foldl
modified
theorem
array.to_list_length
modified
theorem
array.to_list_nth
deleted
theorem
array.to_list_nth_core
added
theorem
array.to_list_nth_le
added
theorem
array.to_list_nth_le_core
modified
theorem
array.to_list_reverse
modified
theorem
array.to_list_to_array
Modified
data/hash_map.lean
added
theorem
hash_map.valid.nodupd
Modified
data/list/basic.lean
added
theorem
list.enum_from_map_fst
added
theorem
list.enum_from_map_snd
added
theorem
list.enum_from_nth
added
theorem
list.enum_map_fst
added
theorem
list.enum_map_snd
added
theorem
list.enum_nth
modified
theorem
list.eq_nil_of_map_eq_nil
modified
theorem
list.ext
modified
theorem
list.foldl_append
added
theorem
list.foldl_join
added
theorem
list.foldr_join
added
theorem
list.infix_of_mem_join
added
theorem
list.length_enum
added
theorem
list.length_enum_from
added
theorem
list.map_join
added
theorem
list.mem_iff_nth
added
theorem
list.mem_iff_nth_le
added
def
list.modify_head
added
def
list.modify_nth
added
theorem
list.modify_nth_eq_take_drop
added
theorem
list.modify_nth_eq_update_nth
added
def
list.modify_nth_tail
added
theorem
list.modify_nth_tail_eq_take_drop
added
theorem
list.nth_eq_some
modified
theorem
list.nth_ge_len
added
theorem
list.nth_le_mem
modified
theorem
list.nth_le_nth
added
theorem
list.nth_le_of_mem
modified
theorem
list.nth_le_reverse_aux1
modified
theorem
list.nth_le_reverse_aux2
added
theorem
list.nth_mem
added
theorem
list.nth_modify_nth
added
theorem
list.nth_modify_nth_eq
added
theorem
list.nth_modify_nth_ne
added
theorem
list.nth_of_mem
added
theorem
list.nth_update_nth_eq
added
theorem
list.nth_update_nth_ne
added
theorem
list.nth_update_nth_of_lt
added
theorem
list.pairwise.and_mem
deleted
theorem
list.pairwise.iff_mem
added
theorem
list.pairwise.iff_of_mem
added
theorem
list.pairwise.imp_mem
added
theorem
list.pairwise.imp_of_mem
added
theorem
list.remove_nth_eq_nth_tail
modified
def
list.to_array
added
theorem
list.update_nth_eq_modify_nth