- Apr 16, 2024
-
-
Ralf Jung authored
-
- Apr 15, 2024
-
-
Robbert Krebbers authored
add lemmas for na_own p ∅ See merge request iris/iris!1044
-
Benjamin Peters authored
-
- Apr 12, 2024
-
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
fix heap_lang notation link in heap_lang.md See merge request iris/iris!1043
-
William Mansky authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
prepare changelog for new release See merge request iris/iris!1045
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Apr 11, 2024
-
-
Ralf Jung authored
-
- Apr 03, 2024
-
-
Ralf Jung authored
-
- Mar 12, 2024
-
-
Robbert Krebbers authored
-
- Mar 11, 2024
-
-
Robbert Krebbers authored
Add lemmas for creating later credits for non-pure steps (alternative) See merge request iris/iris!1036
-
Robbert Krebbers authored
-
- Mar 06, 2024
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Fix #566 by introducing IsDisjUnion class Closes #566 See merge request iris/iris!1039
-
Jan-Oliver Kaiser authored
-
Jan-Oliver Kaiser authored
-
Robbert Krebbers authored
-
Jan-Oliver Kaiser authored
-
- Mar 05, 2024
-
-
Robbert Krebbers authored
Prevent iFrame from instantiating existentials under ∀, -∗, →, WP Closes #565 See merge request iris/iris!1035
-
Ike Mulder authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Add `twp_wp_step_lc` and use that to prove `steps_lb` later credit lemmas for HeapLang atomic instructions.
-
Ike Mulder authored
-
Ike Mulder authored
-
- Mar 04, 2024
-
-
Ralf Jung authored
always do Proof. after Restart. See merge request iris/iris!1040
-
Ralf Jung authored
-
Ike Mulder authored
-
Ike Mulder authored
-
Robbert Krebbers authored
-
- Mar 02, 2024
-
-
Ralf Jung authored
frame_impl: explain why we do not use QuickPersistent Closes #563 See merge request iris/iris!1038
-
-
Robbert Krebbers authored
Add lemma `lc_fupd_add_laterN`. See merge request iris/iris!1037
-
