- Jul 25, 2023
-
-
- 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 iris/iris!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
-
Ralf Jung authored -
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 30, 2023
-
-
Ralf Jung authored
Add mono_nat_own_alloc_strong See merge request iris/iris!949
-
- Jun 29, 2023
-
-
Jaemin Choi authored
-
