Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-24 03:57 e628a2c6

View on Github →

feat(data/finmap): finite maps (#487)

  • feat(data/list/basic): erasep
  • feat(data/list/basic): lookup, ndkeys
  • feat(data/list/sigma,alist): basic functions on association lists
  • feat(data/finmap): finite maps on multisets
  • doc(data/finmap): docstrings [ci-skip]
  • refactor(data/list/{alist,sigma},data/finmap): renaming
  • knodup -> nodupkeys
  • val -> entries
  • nd -> nodupkeys
  • feat(data/finmap): change keys to finset
  • fix(data/list/basic): fix build
  • fix(analysis/{emetric-space,measure-theory/integration}): fix build

Estimated changes

added def alist.to_finmap
added theorem alist.to_finmap_eq
added theorem finmap.empty_to_finmap
added def finmap.erase
added theorem finmap.erase_to_finmap
added theorem finmap.ext
added def finmap.extract
added def finmap.foldl
added theorem finmap.induction_on
added def finmap.insert
added theorem finmap.insert_of_pos
added def finmap.keys
added theorem finmap.keys_empty
added theorem finmap.keys_erase
added theorem finmap.keys_ext
added theorem finmap.keys_replace
added theorem finmap.keys_singleton
added theorem finmap.keys_val
added def finmap.lift_on
added def finmap.lookup
added theorem finmap.lookup_is_some
added theorem finmap.mem_def
added theorem finmap.mem_erase
added theorem finmap.mem_insert
added theorem finmap.mem_keys
added theorem finmap.mem_replace
added theorem finmap.mem_to_finmap
added theorem finmap.not_mem_empty
added def finmap.replace
added def finmap.singleton
added structure finmap
added theorem multiset.coe_nodupkeys
added def alist.erase
added theorem alist.ext
added def alist.extract
added def alist.foldl
added def alist.insert
added theorem alist.insert_of_pos
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_is_some
added theorem alist.mem_def
added theorem alist.mem_erase
added theorem alist.mem_insert
added theorem alist.mem_keys
added theorem alist.mem_of_perm
added theorem alist.mem_replace
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 def alist.replace
added def alist.singleton
added structure alist
modified theorem list.erase_append_left
modified theorem list.erase_append_right
added theorem list.erase_eq_erasep
modified theorem list.erase_sublist_erase
added def list.erasep
added theorem list.erasep_cons
added theorem list.erasep_map
added theorem list.erasep_nil
added theorem list.erasep_sublist
added theorem list.erasep_subset
added theorem list.exists_of_erasep
added def list.extractp
added theorem list.length_lookmap
added def list.lookmap
added theorem list.lookmap_congr
added theorem list.lookmap_cons_none
added theorem list.lookmap_cons_some
added theorem list.lookmap_id'
added theorem list.lookmap_map_eq
added theorem list.lookmap_nil
added theorem list.lookmap_none
added theorem list.lookmap_some
modified theorem list.map_erase
added theorem list.mem_erasep_of_neg
added theorem list.mem_of_mem_erasep
added theorem list.nodup_repeat
added theorem list.perm.swap'
added theorem list.perm_erasep
added theorem list.perm_lookmap
added theorem list.head_lookup_all
added def list.kerase
added theorem list.kerase_map_fst
added theorem list.kerase_nodupkeys
added theorem list.kerase_sublist
added def list.kextract
added def list.kreplace
added theorem list.kreplace_map_fst
added theorem list.kreplace_self
added def list.lookup
added def list.lookup_all
added theorem list.lookup_all_eq_nil
added theorem list.lookup_all_nil
added theorem list.lookup_all_nodup
added theorem list.lookup_cons_eq
added theorem list.lookup_cons_ne
added theorem list.lookup_eq_none
added theorem list.lookup_is_some
added theorem list.lookup_nil
added theorem list.mem_lookup_all
added theorem list.mem_lookup_iff
added def list.nodupkeys
added theorem list.nodupkeys_cons
added theorem list.nodupkeys_join
added theorem list.nodupkeys_nil
added theorem list.of_mem_lookup
added theorem list.perm_kerase
added theorem list.perm_kreplace
added theorem list.perm_lookup
added theorem list.perm_lookup_all
added theorem list.perm_nodupkeys
modified theorem option.ext
added theorem congr_arg_heq