- May 05, 2021
-
-
Simon Gregersen authored
-
- May 04, 2021
-
-
Robbert Krebbers authored
`_True`/`_False` lemmas for `decide` and `mguard` See merge request iris/stdpp!256
-
Robbert Krebbers authored
-
- May 03, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 02, 2021
-
-
Ralf Jung authored
-
- Apr 30, 2021
-
-
Ralf Jung authored
make Z.of_nat not a coercion inside std++ See merge request iris/stdpp!257
-
- Apr 29, 2021
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Don't use Z.to_nat in definition of rotate See merge request iris/stdpp!259
-
Michael Sammler authored
-
Ralf Jung authored
make Qc_of_Z not a Coercion any more Closes #102 See merge request iris/stdpp!258
-
Ralf Jung authored
-
Ralf Jung authored
-
- Apr 23, 2021
-
-
Robbert Krebbers authored
-
- Apr 22, 2021
-
-
Ralf Jung authored
-
- Apr 21, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Fix pretty printing of multset literals + add tests See merge request iris/stdpp!253
-
- Apr 20, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Introduce `SingletonMS` class for multiset singletons. Closes #100, #98, and #87 See merge request iris/stdpp!251
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
- Define set-like notation `{[+ x1; ..; xn ]}` for multisets in terms of the new singleton class and disjoint union `⊎`. - Remove `SemiSet` instance for multisets. - Prove lemmas regarding `∈` and `∉` for multisets since we no longer get the generic versions for sets. - Provide `SetUnfoldElemOf` instances for multisets since we no longer get the generic versions for sets. - Prove lemmas new regarding `∈` and `∉` for `∩` Fixes #100, #98 and #87. This MR is an alternative to !232.
-
Robbert Krebbers authored
Fix inconsistent arguments of `subset_difference_elem_of`. See merge request iris/stdpp!252
-
Robbert Krebbers authored
Add list_to_map_app See merge request iris/stdpp!249
-
Michael Sammler authored
-
Robbert Krebbers authored
-
- Apr 19, 2021
-
-
Robbert Krebbers authored
Add tactic `learn_hyp`, fixes #73 Closes #73 See merge request iris/stdpp!247
-
Robbert Krebbers authored
Add lemmas about testbit on bounded integers See merge request iris/stdpp!248
-
-
- Apr 15, 2021
-
-
Michael Sammler authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
More lemmas for list's prefix_of and suffix_of See merge request iris/stdpp!239
-