Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-28 00:06 bca8d491

View on Github →

chore(data/array, data/buffer): Array and buffer cleanup (#277)

Estimated changes

Modified data/array/lemmas.lean

modified theorem array.mem.def

modified theorem array.mem_rev_list

added theorem array.mem_rev_list_aux

deleted theorem array.mem_rev_list_core

modified theorem array.mem_to_list

modified theorem array.mem_to_list_enum

modified theorem array.push_back_rev_list

added theorem array.push_back_rev_list_aux

deleted theorem array.push_back_rev_list_core

modified theorem array.push_back_to_list

modified theorem array.read_foreach

modified theorem array.read_foreach_aux

modified theorem array.read_map

modified theorem array.read_map₂

modified theorem array.rev_list_foldr

modified theorem array.rev_list_foldr_aux

modified theorem array.rev_list_length_aux

modified theorem array.rev_list_reverse

added theorem array.rev_list_reverse_aux

deleted theorem array.rev_list_reverse_core

modified theorem array.to_list_foldl

modified theorem array.to_list_nth

modified theorem array.to_list_nth_le'

modified theorem array.to_list_nth_le

added theorem array.to_list_nth_le_aux

deleted theorem array.to_list_nth_le_core

modified theorem array.to_list_of_heq

modified theorem array.to_list_reverse

modified theorem array.write_to_list

modified def equiv.d_array_equiv_fin

Modified data/buffer/basic.lean

modified theorem buffer.ext

modified theorem buffer.to_list_append_list

Modified data/hash_map.lean