Merge Requests · Iris / Iris · GitLab

Use original pattern in iDestruct error messages

!550 · opened Oct 20, 2020 by Tej Chajed
- 17
updated Oct 21, 2020
Add library for monotonic nat ghost state

!547 · opened Oct 17, 2020 by Tej Chajed
- 16
updated Oct 21, 2020
Implement monotone partial bijections as a view

!543 · opened Oct 14, 2020 by Tej Chajed
- 48
updated Oct 21, 2020
better support for view shift with mismatching masks

!527 · opened Oct 02, 2020 by Ralf Jung S-waiting-for-review
- 0
updated Oct 13, 2020
multi-package repositories

!514 · opened Sep 26, 2020 by Ralf Jung S-waiting-for-review
- 3
updated Oct 13, 2020
Define logic `clProp` for axiom-free classical logic + remove `pure_forall_2` from BI interface

!496 · opened Sep 05, 2020 by Robbert S-blocked
- 39
updated Oct 01, 2020
Add `array_init` and corresponding WP specs.

!492 · opened Aug 15, 2020 by Dan Frumin S-waiting-for-author
- 25
updated Oct 20, 2020
WIP: Support destructing exists with intro patterns

!483 · opened Jul 22, 2020 by Tej Chajed T-records
- 5
updated Oct 20, 2020
Add duplicable type class

!481 · opened Jul 20, 2020 by Simon Friis Vindum S-waiting-for-author
- 49
updated Sep 29, 2020
WIP: Prepend introduction pattern `H.ipat`. 0 of 1 task completed

!480 · opened Jul 19, 2020 by Robbert T-records
- 22
updated Oct 20, 2020
WIP: Remove `contractive_ne` and `contractive_proper` as instances.

!455 · opened May 27, 2020 by Robbert S-waiting-for-author
- 11
updated Oct 20, 2020
WIP: Add lemmas about local updates of lists

!371 · opened Feb 06, 2020 by Dmitry Khalanskiy S-waiting-for-review
- 51
updated Sep 29, 2020
WIP: Documentation on Iris equalities

!300 · opened Aug 09, 2019 by Paolo G. Giarrusso S-waiting-for-author
- 72
updated Oct 20, 2020