- Jul 28, 2021
-
-
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
-
- Jul 26, 2021
-
-
Robbert Krebbers authored
Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼` See merge request iris/stdpp!306
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename `gmultiset_elem_of_singleton_subseteq` → `gmultiset_singleton_subseteq_l` and swap order to be consistent with Iris's `singleton_included_l`.
-
- Jul 24, 2021
-
-
Ralf Jung authored
Add lemmas that say that `curry{3,4}?` and `uncurry{3,4}?` are inverses. See merge request iris/stdpp!304
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 23, 2021
-
-
Robbert Krebbers authored
solve_ndisj: handle goals containing _ ∖ _ ∖ _ See merge request iris/stdpp!303
-
Ralf Jung authored
-
- Jul 22, 2021
-
-
Ralf Jung authored
-
- Jul 21, 2021
-
-
Ralf Jung authored
`Params` and `Proper` instances for `curry` and friends See merge request iris/stdpp!302
-