- 05 May, 2021 1 commit
-
-
Simon Gregersen authored
-
- 04 May, 2021 2 commits
-
-
Robbert Krebbers authored
`_True`/`_False` lemmas for `decide` and `mguard` See merge request iris/stdpp!256
-
Robbert Krebbers authored
-
- 03 May, 2021 5 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 02 May, 2021 1 commit
-
-
Ralf Jung authored
-
- 30 Apr, 2021 1 commit
-
-
Ralf Jung authored
make Z.of_nat not a coercion inside std++ See merge request iris/stdpp!257
-
- 29 Apr, 2021 8 commits
-
-
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
-
- 23 Apr, 2021 1 commit
-
-
Robbert Krebbers authored
-
- 22 Apr, 2021 1 commit
-
-
Ralf Jung authored
-
- 21 Apr, 2021 3 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Fix pretty printing of multset literals + add tests See merge request iris/stdpp!253
-
- 20 Apr, 2021 11 commits
-
-
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
-
- 19 Apr, 2021 3 commits
-
-
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
-
-
- 15 Apr, 2021 3 commits
-
-
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
-