Commit 2023-01-13 13:00 40d6bcd5

View on Github →

feat: port Data.List.AList (#1530)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/AList.lean

added def AList.Disjoint

added theorem AList.empty_entries

added theorem AList.empty_union

added theorem AList.entries_to_alist

added def AList.erase

added theorem AList.erase_erase

added theorem AList.ext

added theorem AList.ext_iff

added def AList.extract

added theorem AList.extract_eq_lookup_erase

added def AList.foldl

added def AList.insert

added theorem AList.insert_empty

added theorem AList.insert_entries

added theorem AList.insert_entries_of_neg

added theorem AList.insert_insert

added theorem AList.insert_insert_of_ne

added theorem AList.insert_singleton_eq

added theorem AList.insert_union

added def AList.keys

added theorem AList.keys_empty

added theorem AList.keys_erase

added theorem AList.keys_insert

added theorem AList.keys_nodup

added theorem AList.keys_replace

added theorem AList.keys_singleton

added def AList.lookup

added theorem AList.lookup_empty

added theorem AList.lookup_eq_none

added theorem AList.lookup_erase

added theorem AList.lookup_erase_ne

added theorem AList.lookup_insert

added theorem AList.lookup_insert_ne

added theorem AList.lookup_is_some

added theorem AList.lookup_to_alist

added theorem AList.lookup_union_eq_some

added theorem AList.lookup_union_left

added theorem AList.lookup_union_right

added theorem AList.mem_erase

added theorem AList.mem_insert

added theorem AList.mem_keys

added theorem AList.mem_lookup_iff

added theorem AList.mem_lookup_union

added theorem AList.mem_lookup_union_middle

added theorem AList.mem_of_perm

added theorem AList.mem_replace

added theorem AList.mem_union

added theorem AList.not_mem_empty

added theorem AList.perm_erase

added theorem AList.perm_insert

added theorem AList.perm_lookup

added theorem AList.perm_replace

added theorem AList.perm_union

added def AList.replace

added def AList.singleton

added theorem AList.singleton_entries

added theorem AList.to_alist_cons

added def AList.union

added theorem AList.union_assoc

added theorem AList.union_comm_of_disjoint

added theorem AList.union_empty

added theorem AList.union_entries

added theorem AList.union_erase

added structure AList

added def List.toAList