Merge requests · Iris / Iris · GitLab

Add some missing internal validity and equivalence lemmas for dfrac, auth, agree and reservation_map

!942 · created Jun 02, 2023 by Ike Mulder
- 6
updated Jun 03, 2023
Added missing reflexivity, symmetry, transitivity lemmas on ↔, →, -∗ and ∗-∗

!941 · created Jun 01, 2023 by Ike Mulder
updated Jun 02, 2023
add test for iInv with accessor variables

!937 · created May 30, 2023 by Ralf Jung
- 0
updated May 30, 2023
Make bi fields non-canonical

!933 · created May 26, 2023 by Paolo G. Giarrusso
- 19
updated Jun 03, 2023
Use Ltac2 to avoid unrolling tactic notations with lists.

!931 · created May 26, 2023 by Janno
- 3
- 14
updated May 31, 2023
Draft: Improve validity information received from `iCombine`ing `own`s

!930 · created May 25, 2023 by Ike Mulder
updated Jun 03, 2023
make lock spec a Class

!929 · created May 21, 2023 by Ralf Jung
- 0
updated May 21, 2023
Add Fractional instance for AsFractional

!926 · created May 11, 2023 by Isaac van Bakel
updated May 31, 2023
Show that for non-step indexed BIs, <pers> can trivially be inhabited.

!925 · created May 05, 2023 by Robbert Krebbers
- 14
updated May 12, 2023
Add reference-counting reader-writer lock implementation

!923 · created May 05, 2023 by Isaac van Bakel
- 37
updated May 31, 2023
`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.

!916 · created Apr 30, 2023 by Robbert Krebbers
- 5
updated May 02, 2023
Draft: Add a Strategy command for ucmra projections

!907 · created Apr 19, 2023 by Ike Mulder
- 10
updated May 02, 2023
add fixpoint lemmas for plain and absorbing

!903 · created Apr 01, 2023 by William Mansky
S-waiting-for-review
- 10
updated May 30, 2023
Draft: parameterize the algebra folder by the stepindex type for integration with Transfinite Iris

!888 · created Feb 05, 2023 by Lennard Gäher
- 1
- 74
updated May 31, 2023
WIP: Step Update modality demonstration

!887 · created Jan 30, 2023 by Jonas Kastberg
- 1
- 0
updated May 26, 2023
get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays

!883 · created Jan 12, 2023 by Ralf Jung
updated Jan 12, 2023
Added fupd_plain_soundness_no_lc_strong

!857 · created Oct 25, 2022 by Jonas Kastberg
S-waiting-for-author
- 55
updated Mar 23, 2023
Renamed/added macros to iris.sty

!851 · created Oct 12, 2022 by Jonas Kastberg
S-waiting-for-author
- 37
updated Mar 24, 2023
Draft: move bi_persistently_emp out of BI interface, and get a basic proof mode working again

!843 · created Aug 13, 2022 by Ralf Jung
updated May 10, 2023
Make* class tweaks

!842 · created Aug 13, 2022 by Ralf Jung
S-blocked
updated Aug 16, 2022