- Jun 08, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
Make filter lemmas for maps and sets consistent + add cross split property for maps See merge request iris/stdpp!274
-
- Jun 07, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and `map_union_filter` → `map_filter_union_complement`.
-
Robbert Krebbers authored
sum_list_with_in See merge request !275
-
-
- Jun 06, 2021
-
-
Robbert Krebbers authored
Strengthen `map_filter_strong_ext` and `map_filter_ext`. See merge request iris/stdpp!269
-
Dan Frumin authored
-
Dan Frumin authored
-
Dan Frumin authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jun 05, 2021
-
-
Ralf Jung authored
-
- Jun 04, 2021
-
-
Robbert Krebbers authored
More missing `Hint Mode`s. See merge request !271
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Jun 03, 2021
-
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- Jun 02, 2021
-
-
Ralf Jung authored
Add lemma `set_fold_disj_union_strong`. See merge request iris/stdpp!267
-
-
Robbert Krebbers authored
Add a few lemmas See merge request iris/stdpp!266
-
Robbert Krebbers authored
Add function `map_kmap` that transforms the keys of a finite map. See merge request iris/stdpp!265
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Thanks to @tchajed for pointing out the omission.
-