Merge requests · Iris / Iris · GitLab

Draft: Add simple library for priority levels and use it for `iFrame`

!742 · created Oct 11, 2021 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 18
updated May 06, 2022
Use class `IntoFUpd` in tactic `wp_value_head`

!613 · created Jan 05, 2021 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 13
updated Dec 12, 2021
WIP: Define more uPred connectives in siProp

!710 · created Jun 29, 2021 by Hai Dang S-draft S-waiting-for-author
- CLOSED
- 55
updated Nov 30, 2021
Define logic `clProp` for axiom-free classical logic

!496 · created Sep 05, 2020 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 45
updated May 12, 2021
Draft: More (peri)scopes for Iris

!651 · created Mar 16, 2021 by Paolo G. Giarrusso S-waiting-for-author
- CLOSED
- 18
updated May 07, 2021
Alternative take at "better support for view shift with mismatching masks"

!615 · created Jan 05, 2021 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 6
updated Apr 29, 2021
WIP: Remove `contractive_ne` and `contractive_proper` as instances.

!455 · created May 27, 2020 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 13
updated Feb 15, 2021
WIP: Documentation on Iris equalities

!300 · created Aug 09, 2019 by Paolo G. Giarrusso S-waiting-for-author
- CLOSED
- 73
updated Nov 06, 2020
Specify how to compile Iris without running the tests

!466 · created Jun 19, 2020 by Dan Frumin S-waiting-for-author
- CLOSED
- 13
updated Sep 30, 2020
WIP: Add `with M` option to `iModIntro` and use to redefine `iNext` to fix issue #331

!467 · created Jun 29, 2020 by Robbert Krebbers S-waiting-for-author
- CLOSED
- 41
updated Sep 29, 2020
WIP: Generic union, disjoint union CMRAs for sets.

!381 · created Feb 23, 2020 by David Swasey S-waiting-for-author
- CLOSED
- 1
- 30
updated Sep 29, 2020
WIP: Prototype a validity restriction CMRA construction

!502 · created Sep 08, 2020 by Tej Chajed S-waiting-for-author
- CLOSED
- 24
updated Sep 14, 2020
Implement CMRA via an isomorphism to another CMRA

!348 · created Dec 15, 2019 by Tej Chajed S-waiting-for-author
- CLOSED
- 38
updated Sep 12, 2020
if instances for absorbing, affine and persistent

!474 · created Jul 13, 2020 by Alix Trieu S-waiting-for-author
- CLOSED
- 8
updated Sep 08, 2020