Commits · cc70f824dff9f40ed05e6cbc1b58e2121072d474 · Iris / stdpp

Jun 07, 2021
- Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and... · cc70f824
  Robbert Krebbers authored 3 years ago
  
  Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and `map_union_filter` → `map_filter_union_complement`.
  cc70f824
Jun 06, 2021
- Merge branch 'map_filter_strong_ext' into 'master' · 86e53498
  Robbert Krebbers authored 3 years ago
  
  Strengthen `map_filter_strong_ext` and `map_filter_ext`. See merge request !269
  86e53498
- Update changelog · 4100164d
  Dan Frumin authored 3 years ago
  
  4100164d
- Better naming · 8396f122
  Dan Frumin authored 3 years ago
  
  8396f122
- Add `map_filter_strong_ext_2`. · 6058134f
  Dan Frumin authored 3 years ago
  
  6058134f
- update 'Equiv' mode comment · 29af30c2
  Ralf Jung authored 3 years ago
  
  29af30c2
- coq-lint: follow the style of other make messages · 34796f9a
  Ralf Jung authored 3 years ago
  
  34796f9a
Jun 05, 2021
- mark most jobs as interruptible · 10ee8561
  Ralf Jung authored 3 years ago
  
  10ee8561
Jun 04, 2021
- Merge branch 'robbert/hintmode' into 'master' · aeb449a7
  Robbert Krebbers authored 3 years ago
  
  More missing `Hint Mode`s. See merge request !271
  aeb449a7
- CHANGELOG. · c75cd874
  Robbert Krebbers authored 3 years ago
  
  c75cd874
- Use `!` instead of `+`. · b48d40e9
  Robbert Krebbers authored 3 years ago
  
  b48d40e9
- try to fix shell script line endings · f65bf936
  Ralf Jung authored 3 years ago
  
  f65bf936
Jun 03, 2021
- fix invoking our linter · 195f23ec
  Ralf Jung authored 3 years ago
  
  195f23ec
- Merge branch 'master' of https://gitlab.mpi-sws.org/iris/stdpp · 0437f130
  Ralf Jung authored 3 years ago
  
  0437f130
- move our style checks into separate file · 0f2248ef
  Ralf Jung authored 3 years ago
  
  0f2248ef
- More missing `Hint Mode`s. · 5e3d8b90
  Robbert Krebbers authored 3 years ago
  
  5e3d8b90
Jun 02, 2021
- Merge branch 'robbert/set_fold_disj_union_strong' into 'master' · 8542ca97
  Ralf Jung authored 3 years ago
  
  Add lemma `set_fold_disj_union_strong`. See merge request !267
  8542ca97
- Add lemma `set_fold_disj_union_strong`. · 3b72ac77
  Robbert Krebbers authored 3 years ago and Ralf Jung committed 3 years ago
  
  3b72ac77
- Merge branch 'master' into 'master' · 14505877
  Robbert Krebbers authored 3 years ago
  
  Add a few lemmas See merge request !266
  14505877
- Merge branch 'robbert/kmap' into 'master' · ab9793a5
  Robbert Krebbers authored 3 years ago
  
  Add function `map_kmap` that transforms the keys of a finite map. See merge request !265
  ab9793a5
- CHANGELOG. · a35dedaf
  Robbert Krebbers authored 3 years ago
  
  a35dedaf
- Comment about partial inverse. · 474be0c3
  Robbert Krebbers authored 3 years ago
  
  474be0c3
- Parentheses. · 5de3c7f7
  Robbert Krebbers authored 3 years ago
  
  5de3c7f7
- Rename `map_kmap` into `kmap` since `kmap` does not make sense for other data structures. · e479ab8f
  Robbert Krebbers authored 3 years ago
  
  e479ab8f
- Add lemma `dom_map_kmap`. · 249891cd
  Robbert Krebbers authored 3 years ago
  
  249891cd
- Lemmas for `map_kmap` and disjointness and subsets. · e18f9a7d
  Robbert Krebbers authored 3 years ago
  
  e18f9a7d
- More `map_kmap` lemmas for equality. · cfdafacf
  Robbert Krebbers authored 3 years ago
  
  cfdafacf
- Add lemmas for `merge` like operations. · b1fd9651
  Robbert Krebbers authored 3 years ago
  
  b1fd9651
- Add function `map_kmap` that transforms the keys of a finite map. · 324c9c50
  Robbert Krebbers authored 3 years ago
  
  324c9c50
- Update CHANGELOG regarding Permutation changes. · 558df4bc
  Robbert Krebbers authored 3 years ago
  
  Thanks to @tchajed for pointing out the omission.
  558df4bc
- Merge branch 'robbert/Permutation' into 'master' · 8f85e406
  Robbert Krebbers authored 3 years ago
  
  Various improvements to `Permutation` lemmas and instances See merge request !270
  8f85e406
Jun 01, 2021
- CHANGELOG. · c2d43491
  Robbert Krebbers authored 3 years ago
  
  c2d43491
- Rename `Permutation_nil` and `Permutation_singleton` into `Permutation_nil_r`... · 33b3cd0d
  Robbert Krebbers authored 3 years ago
  
  Rename `Permutation_nil` and `Permutation_singleton` into `Permutation_nil_r` and `Permutation_singleton_r`. Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
  33b3cd0d
- Name instances for `Permutation` and add new instance `cons_Permutation_inj_l`. · 0bb21a4f
  Robbert Krebbers authored 3 years ago
  
  Naming scheme: `operation_Permutation_{Proper,inj,inj_l,inj_r}`.
  0bb21a4f
- Remove instances from stdlib. · 3f893ee4
  Robbert Krebbers authored 3 years ago
  
  3f893ee4
- Add lemma `Permutation_cross_split`. · 3b9d4118
  Robbert Krebbers authored 3 years ago
  
  3b9d4118
- Make `elem_of_Permutation` a ``. · 5bb9627f
  Robbert Krebbers authored 3 years ago
  
  5bb9627f
- Explicitly spell out lemma statement of some `Permutation` lemmas that we borrow from stdlib. · d4dcb60b
  Robbert Krebbers authored 3 years ago
  
  d4dcb60b
- Group `Permutation` lemmas together. · d5660c4d
  Robbert Krebbers authored 3 years ago
  
  d5660c4d
- Move `delete` lemmas out of `Permutation` section. · ad7129fd
  Robbert Krebbers authored 3 years ago
  
  ad7129fd