Merge requests · Iris / Iris · GitLab

Draft: parameterize the algebra folder by the stepindex type for integration with Transfinite Iris

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

!887 · created Jan 30, 2023 by Jonas Kastberg
- 1
- 0
updated Jan 30, 2023
Change definition of dist_later for compatability with Transfinite Iris

!886 · created Jan 25, 2023 by Michael Sammler
- 2
- 33
updated Feb 06, 2023
Introcude bi_nsteps and add timeless results for bi closures

!885 · created Jan 17, 2023 by Simcha van Collem
- 3
updated Feb 01, 2023
add 'wp_apply (...) as'

!884 · created Jan 12, 2023 by Ralf Jung
- 0
updated Jan 12, 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
- 4
updated Jan 12, 2023
add lemmas for 'separable' propositions

!881 · created Jan 06, 2023 by Ralf Jung
- 6
updated Jan 08, 2023
add mono_Z base-logic library

!880 · created Dec 22, 2022 by Ralf Jung
- 0
updated Dec 22, 2022
add RA for integers with addition

!879 · created Dec 22, 2022 by Ralf Jung
- 0
updated Dec 22, 2022
add big_opM_gset_to_gmap

!878 · created Dec 13, 2022 by Ralf Jung
- 0
updated Dec 13, 2022
Improve iCombine to allow a 'gives' clause for validity properties

!872 · created Dec 01, 2022 by Ike Mulder
- 114
updated Feb 01, 2023
Draft: Fix #497: avoid Hint Immediate

!869 · created Nov 24, 2022 by Paolo G. Giarrusso
- 0
updated Nov 24, 2022
Added fupd_plain_soundness_no_lc_strong

!857 · created Oct 25, 2022 by Jonas Kastberg
updated Nov 30, 2022
Add order operations for locations in HeapLang.

!854 · created Oct 14, 2022 by Arthur Azevedo de Amorim S-waiting-for-author
- 7
updated Feb 07, 2023
Renamed/added macros to iris.sty

!851 · created Oct 12, 2022 by Jonas Kastberg
- 24
updated Nov 13, 2022
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 Jan 08, 2023
Make* class tweaks

!842 · created Aug 13, 2022 by Ralf Jung S-blocked
updated Aug 16, 2022
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
- 56
updated Nov 23, 2022
Dune build files

!820 · created Jul 23, 2022 by Paolo G. Giarrusso S-blocked S-draft
- 1
updated Nov 23, 2022
make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)

!791 · created May 07, 2022 by Ralf Jung S-waiting-for-author
- 29
updated Dec 05, 2022