- Jul 27, 2023
-
-
Ralf Jung authored
-
- Jul 25, 2023
-
-
Ralf Jung authored
rename `singleton_mono` to `singleton_included_mono` See merge request iris/iris!955
-
Ralf Jung authored
Add fupd_plain_soundness_no_lc_strong See merge request iris/iris!857
-
-
Robbert Krebbers authored
Show that for non-step indexed BIs, <pers> can trivially be inhabited. See merge request iris/iris!925
-
-
Ralf Jung authored
-
- Jul 24, 2023
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Add derived ≼ connective on the BI level. See merge request iris/iris!944
-
Robbert Krebbers authored
-
Ike Mulder authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ike Mulder authored
-
Robbert Krebbers authored
Make sure that `iRevert` preserves names and does not invent fresh ones. See merge request iris/iris!952
-
Robbert Krebbers authored
add some more option_included lemmas See merge request !947
-
Robbert Krebbers authored
Simplify proofs of `gmap` local update lemmas. See merge request iris/iris!951
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Let `iExFalso` perform `iStartProof`. See merge request iris/iris!954
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Add local update lemmas for `discrete_fun` and `unit`. See merge request iris/iris!948
-
Dan Frumin authored
-
- Jul 23, 2023
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 22, 2023
- Jul 21, 2023
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Add ∗-∗ as notation in stdpp_scope similar to -∗. See merge request iris/iris!764
-
