Merge requests · Iris / Iris · GitLab

fix triple issues with revert, and add logatom triples

!801 · created May 23, 2022 by Ralf Jung
- 0
updated May 23, 2022
document HeapLang syntax and operational semantics

!800 · created May 18, 2022 by Ralf Jung
- 4
updated May 21, 2022
proofmode: do not treat pure assertions as persistent

!799 · created May 16, 2022 by Ralf Jung
- 3
updated May 23, 2022
adjust proofmode of_envs to rely less on persistently_emp_2

!794 · created May 12, 2022 by Ralf Jung
- 1
- 8
updated May 17, 2022
First Steps for Later Credits

!792 · created May 09, 2022 by Simon Spies
updated May 23, 2022
make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)

!791 · created May 07, 2022 by Ralf Jung
- 2
updated May 08, 2022
Attempt at avoiding `unfold` to unfold primitive projections. 2 of 3 tasks completed

!778 · created Feb 14, 2022 by Robbert Krebbers S-waiting-for-author
- 14
updated May 18, 2022
Draft: Add simplification machinery for ✓ and ≼.

!771 · created Jan 10, 2022 by Ike Mulder S-blocked
updated May 06, 2022
Add ∗-∗ as notation in stdpp_scope similar to -∗.

!764 · created Dec 05, 2021 by Robbert Krebbers
- 6
updated May 08, 2022
Flip atomic updates quantifiers compared to atomic triples

!750 · created Nov 09, 2021 by Paolo G. Giarrusso S-waiting-for-author
updated May 09, 2022