Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-07 13:13 8a1de249

View on Github →

feat(data/{list/alist,finmap}): implicit key type (#662)

  • feat(data/{list/alist,finmap}): implicit key type Make the key type α implicit in both alist and finmap. This brings these types into line with the underlying sigma and simplifies usage since α is inferred from the value function type β : α → Type v.
  • doc(data/list/alist): alist is stored as a linked list

Estimated changes

modified def alist.to_finmap
modified theorem alist.to_finmap_entries
modified theorem alist.to_finmap_eq
modified theorem finmap.empty_to_finmap
modified def finmap.erase
modified theorem finmap.erase_to_finmap
modified theorem finmap.ext
modified def finmap.extract
modified def finmap.insert
modified theorem finmap.insert_of_pos
modified theorem finmap.insert_to_finmap
modified def finmap.keys
modified theorem finmap.keys_empty
modified theorem finmap.keys_erase
modified theorem finmap.keys_erase_to_finset
modified theorem finmap.keys_ext
modified theorem finmap.keys_replace
modified theorem finmap.keys_val
modified theorem finmap.lift_on_to_finmap
modified def finmap.lookup
modified theorem finmap.lookup_is_some
modified theorem finmap.lookup_to_finmap
modified theorem finmap.mem_def
modified theorem finmap.mem_erase
modified theorem finmap.mem_insert
modified theorem finmap.mem_keys
modified theorem finmap.mem_replace
modified theorem finmap.mem_to_finmap
modified theorem finmap.not_mem_empty
modified def finmap.replace
modified theorem finmap.replace_to_finmap
modified def finmap.singleton
modified structure finmap
modified def alist.erase
modified theorem alist.ext
modified def alist.extract
modified def alist.foldl
modified def alist.insert
modified theorem alist.insert_entries_of_neg
modified theorem alist.insert_of_pos
modified def alist.keys
modified theorem alist.keys_empty
modified theorem alist.keys_erase
modified theorem alist.keys_insert
modified theorem alist.keys_nodup
modified theorem alist.keys_replace
modified def alist.lookup
modified theorem alist.lookup_is_some
modified theorem alist.mem_def
modified theorem alist.mem_erase
modified theorem alist.mem_insert
modified theorem alist.mem_keys
modified theorem alist.mem_of_perm
modified theorem alist.mem_replace
modified theorem alist.not_mem_empty
modified theorem alist.not_mem_empty_entries
modified theorem alist.perm_erase
modified theorem alist.perm_insert
modified theorem alist.perm_lookup
modified theorem alist.perm_replace
modified def alist.replace
modified def alist.singleton
modified structure alist