Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-07 19:26 d95bff06

View on Github →

refactor(data/hash_map): improve hash_map proof Decrease dependence on implementation details of array

Estimated changes

modified theorem array.rev_list_length
modified theorem array.rev_list_reverse
modified theorem array.to_list_length
added theorem array.to_list_nth_le'
modified theorem array.to_list_reverse
added theorem array.write_to_list
modified def bucket_array.as_list
deleted theorem bucket_array.foldl_eq_lem
added theorem hash_map.mk_valid
deleted theorem hash_map.valid.eq'
deleted theorem hash_map.valid.eq
modified theorem hash_map.valid.find_aux_iff
deleted theorem hash_map.valid.mk
modified theorem hash_map.valid.modify
deleted theorem hash_map.valid.nodup
deleted theorem hash_map.valid.nodupd
added structure hash_map.valid
deleted def hash_map.valid
deleted theorem hash_map.valid_aux.eq
deleted theorem hash_map.valid_aux.nodup
deleted inductive hash_map.valid_aux
added theorem list.join_append
added theorem list.modify_nth_length
modified theorem list.nth_update_nth_of_lt
added theorem list.update_nth_length