- Jul 27, 2021
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
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
-
-
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
-
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 !297
-
Robbert Krebbers authored
-