Merge requests · Iris / Iris · GitLab

`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.

!916 · created Apr 30, 2023 by Robbert Krebbers
S-waiting-for-author
- Closed
- 7
updated Oct 10, 2024
Renamed/added macros to iris.sty

!851 · created Oct 12, 2022 by Jonas Kastberg
S-waiting-for-author
- Closed
- 39
updated Jul 30, 2024
Add comments to explain the modified structure of the adequacy proof

!847 · created Aug 19, 2022 by Simon Spies
S-waiting-for-author
- Merged
- 17
updated Feb 01, 2023
Allow controlling stuckness at the language level 0 of 6 checklist items completed

!825 · created Aug 02, 2022 by Michael Sammler
S-waiting-for-author
- Closed
- 60
updated Mar 20, 2023
Updated suggested emacs indendation configuration

!776 · created Jan 19, 2022 by Jonas Kastberg
S-waiting-for-author
- Merged
- 18
updated May 11, 2022
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 Sep 29, 2023
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
Add mode for Dist

!700 · created Jun 08, 2021 by Paolo G. Giarrusso
S-waiting-for-author
- Merged
- 23
updated Jun 18, 2021
Add generalized implication lemma for big_sepM

!697 · created Jun 01, 2021 by Simon Friis Vindum
S-waiting-for-author
- Merged
- 57
updated Jul 31, 2021
Add missing commutations for `fupd`

!688 · created May 21, 2021 by Paolo G. Giarrusso
S-waiting-for-author
- Merged
- 30
updated May 31, 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
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
Add a verified interpreter for HeapLang

!564 · created Nov 03, 2020 by Tej Chajed
S-waiting-for-author
- Merged
- 43
updated Mar 18, 2021
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
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
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
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
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: 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