- Jul 28, 2021
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
add insert_map_seq_0 See merge request iris/stdpp!314
-
Ralf Jung authored
add lookup_take_Some See merge request iris/stdpp!313
-
Ralf Jung authored
add binder_list See merge request iris/stdpp!312
-
Robbert Krebbers authored
Mark gset methods as simpl never to stop `cbn` from unfolding them See merge request iris/stdpp!298
-
Paolo G. Giarrusso authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
Ralf Jung authored
Add more lemmas for FinMaps (for union, filter, difference) See merge request iris/stdpp!245
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Hai Dang authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Generalize `map_filter_insert` so that it covers both the True and False case. See merge request iris/stdpp!310
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Use `_True` and `_False` for the specific cases. Weaken premise of `map_filter_delete_not` and make it consistent with `map_filter_insert_not'`.
-
- Jul 27, 2021
-
-
Robbert Krebbers authored
Clean up `empty{',_inv,_iff}` lemmas. See merge request iris/stdpp!307
-
Robbert Krebbers authored
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Write them all using `
` and consistently use the `_iff` suffix. -
Robbert Krebbers authored
-
Ralf Jung authored
some lemmas about list submseteq See merge request iris/stdpp!305
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Add lemma `map_singleton_subseteq_l` and `map_singleton_subseteq`. See merge request iris/stdpp!308
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-