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