Merge requests · Iris / Iris · GitLab

generalize gmap_view for an arbitrary CMRA as values

!959 · created Jul 27, 2023 by Ralf Jung
S-waiting-for-review
- 21
updated Nov 27, 2023
Flip atomic updates quantifiers compared to atomic triples

!750 · created Nov 09, 2021 by Paolo G. Giarrusso
S-waiting-for-review
- Merged
- 21
updated May 24, 2022
Add `big_sepM2_union_inv_*`.

!690 · created May 24, 2021 by Dan Frumin
S-waiting-for-review
- Merged
- 8
updated May 26, 2021
Explicit visibility for Instances

!684 · created May 20, 2021 by Ralf Jung
S-waiting-for-review
- Merged
- 6
updated May 25, 2021
Add functional notations for `dist`

!671 · created Apr 30, 2021 by Yusuke Matsushita
S-waiting-for-review
- Merged
- 7
updated May 11, 2021
don't tie bi.weakestpre to program_logic.language (full TC approach)

!656 · created Mar 17, 2021 by Ralf Jung
S-waiting-for-review
- Merged
- 29
updated Jun 18, 2021
register make_laterable as modality

!636 · created Feb 12, 2021 by Ralf Jung
S-waiting-for-review
- Merged
- 33
updated Jun 18, 2021
FromPure instances for big_sepM

!626 · created Jan 27, 2021 by Ralf Jung
S-waiting-for-review
- Merged
- 15
updated May 26, 2021
Add monotone resource algebra

!597 · created Dec 02, 2020 by Amin Timany
S-waiting-for-review
- Merged
- 22
updated May 13, 2021
add ghost_map library

!562 · created Nov 02, 2020 by Ralf Jung
S-waiting-for-review
- Merged
- 33
updated Mar 06, 2021
Use original pattern in iDestruct error messages

!550 · created Oct 20, 2020 by Tej Chajed
S-waiting-for-review
- Merged
- 28
updated Nov 11, 2020
better support for view shift with mismatching masks

!527 · created Oct 02, 2020 by Ralf Jung
S-waiting-for-review
- Closed
- 12
updated Apr 29, 2021
multi-package repositories

!514 · created Sep 26, 2020 by Ralf Jung
S-waiting-for-review
- Merged
- 1
- 31
updated Nov 11, 2020
Improve framing below modalities

!450 · created May 25, 2020 by Robbert Krebbers
S-waiting-for-review
- Closed
- 5
updated Sep 29, 2020
heap_lang: support deallocation

!439 · created May 07, 2020 by Ralf Jung Iris 3.3
S-waiting-for-review T-heap_lang
- Merged
- 62
updated May 25, 2020
Add lemmas about local updates of lists

!371 · created Feb 06, 2020 by Dmitry Khalanskiy
S-waiting-for-review
- Closed
- 70
updated Mar 17, 2021
Try getting rid of total Core typeclass

!294 · created Jul 14, 2019 by Ralf Jung
S-waiting-for-review
- Merged
- 1
updated Dec 02, 2019
WIP: Make `[#]` produce goal with `<pers>` modality if premise is not persistent

!216 · created Feb 17, 2019 by Dan Frumin
S-waiting-for-review
- Closed
- 15
updated May 25, 2020