- Jul 27, 2021
-
-
-
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
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
solve_ndisj: solve more goals involving chains of differences See merge request iris/stdpp!300
-
-
Ralf Jung authored
-
Ralf Jung authored
-