- Jul 27, 2021
-
-
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 !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
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
- Jul 23, 2021
-
-
Robbert Krebbers authored
solve_ndisj: handle goals containing _ ∖ _ ∖ _ See merge request !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
-
Ralf Jung authored
rename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r) See merge request iris/stdpp!301
-
Ralf Jung authored
-
- Jul 20, 2021
-
-
Robbert Krebbers authored
-
- Jul 19, 2021
-
-
Robbert Krebbers authored
Swap `curry` and `uncurry` to be consistent with Haskell and friends. Closes #76 See merge request iris/stdpp!297
-