Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-25 13:51 94510873

View on Github →

refactor(*): move in list lemmas, adapt to change in list.union

Estimated changes

Modified data/hash_map.lean

added theorem hash_map.insert_lemma

deleted theorem hash_map.insert_theorem

Modified data/list/basic.lean

added def list.concat

added theorem list.concat_eq_append

added def list.filter_map

added def list.find

added def list.find_indexes

added def list.find_indexes_aux

added theorem list.index_of_cons_eq

added theorem list.index_of_cons_ne

deleted theorem list.index_of_cons_of_eq

deleted theorem list.index_of_cons_of_ne

added theorem list.index_of_cons_self

added theorem list.index_of_eq_length

modified theorem list.index_of_lt_length

modified theorem list.index_of_nth

added theorem list.index_of_nth_le

modified theorem list.index_of_of_not_mem

added def list.indexes_of

added def list.inits

added def list.is_infix

added def list.is_prefix

added def list.is_suffix

added theorem list.length_concat

added theorem list.map_concat

added def list.map₂

deleted theorem list.mem_append_of_mem_or_mem

deleted theorem list.mem_or_mem_of_mem_append

modified theorem list.mem_split

modified theorem list.not_mem_append

deleted theorem list.not_mem_of_index_of_eq_length

deleted theorem list.not_mem_of_not_mem_append_left

deleted theorem list.not_mem_of_not_mem_append_right

added def list.nth_le

added def list.remove_nth

added def list.scanl

added def list.scanr

added def list.scanr_aux

added def list.split_at

modified theorem list.sublist.refl

modified theorem list.sublist.trans

added def list.sublists

added def list.sublists_aux

added def list.sum

added def list.tails

added def list.take_while

added def list.to_array

added def list.transpose

added def list.transpose_aux

added def list.update_nth

Modified data/list/comb.lean

Modified data/list/perm.lean

modified theorem list.perm.perm_insert

modified theorem list.perm.perm_insert_insert

Modified data/list/set.lean

added theorem list.cons_union

deleted theorem list.disjoint.comm

added theorem list.disjoint.symm

added theorem list.disjoint_comm

deleted theorem list.disjoint_nil_right

added theorem list.disjoint_singleton

deleted theorem list.erase_cons

modified theorem list.erase_dup_cons_of_mem

modified theorem list.erase_dup_cons_of_not_mem

modified theorem list.erase_dup_eq_of_nodup

modified theorem list.erase_dup_nil

modified theorem list.erase_nil

modified theorem list.insert.def

modified theorem list.insert_of_not_mem

modified theorem list.mem_erase_dup

deleted theorem list.mem_erase_dup_iff

modified theorem list.mem_insert_iff

deleted theorem list.mem_of_mem_erase_dup

modified theorem list.mem_or_mem_of_mem_union

modified theorem list.mem_union_iff

added theorem list.nil_union

added theorem list.nodup_append

deleted theorem list.nodup_append_of_nodup_of_nodup_of_disjoint

added theorem list.nodup_union

deleted theorem list.nodup_union_of_nodup_of_nodup

added theorem list.singleton_disjoint

deleted theorem list.union_cons

deleted theorem list.union_nil

Modified data/set/basic.lean

modified theorem set.mem_empty_eq

modified theorem set.mem_image_eq

modified theorem set.mem_sep_eq

Modified logic/basic.lean

modified theorem set_of_subset_set_of

Modified tactic/finish.lean