Commits on Source (23)
-
Robbert Krebbers authoredd1e5eb25
-
Robbert Krebbers authoredeccbfcb1
-
Robbert Krebbers authored0476514f
-
Robbert Krebbers authored38176378
-
Ralf Jung authored3fa48930
-
ca02a39c
-
Robbert Krebbers authored
Show that for non-step indexed BIs, <pers> can trivially be inhabited. See merge request iris/iris!925
5f3d998c -
5294c941
-
Ralf Jung authored
Add fupd_plain_soundness_no_lc_strong See merge request iris/iris!857
2e79afb9 -
Ralf Jung authored
rename `singleton_mono` to `singleton_included_mono` See merge request iris/iris!955
621d76cf -
Ralf Jung authoredc0e3323a
-
Robbert Krebbers authored
add pair_dist See merge request iris/iris!961
4f680c6b -
Paolo G. Giarrusso authoredbf052ca1
-
Paolo G. Giarrusso authored5b18a235
-
Paolo G. Giarrusso authored6911395b
-
Paolo G. Giarrusso authorede2cbb35c
-
Paolo G. Giarrusso authored86b6b8e7
-
Robbert Krebbers authoredfec7b59e
-
Robbert Krebbers authored247ff95f
-
Robbert Krebbers authored6fef06cf
-
Robbert Krebbers authoredc8343385
-
Robbert Krebbers authorede8549c1a
-
Robbert Krebbers authoredd3f6c7e2
Showing
- CHANGELOG.md 5 additions, 0 deletionsCHANGELOG.md
- docs/style_guide.md 1 addition, 4 deletionsdocs/style_guide.md
- iris/algebra/gmap.v 1 addition, 1 deletioniris/algebra/gmap.v
- iris/algebra/ofe.v 4 additions, 0 deletionsiris/algebra/ofe.v
- iris/base_logic/bi.v 12 additions, 4 deletionsiris/base_logic/bi.v
- iris/base_logic/lib/fancy_updates.v 30 additions, 8 deletionsiris/base_logic/lib/fancy_updates.v
- iris/bi/interface.v 93 additions, 14 deletionsiris/bi/interface.v
- iris/bi/monpred.v 13 additions, 3 deletionsiris/bi/monpred.v
- iris/si_logic/bi.v 13 additions, 4 deletionsiris/si_logic/bi.v
- iris_unstable/algebra/monotone.v 119 additions, 174 deletionsiris_unstable/algebra/monotone.v
- iris_unstable/base_logic/algebra.v 1 addition, 13 deletionsiris_unstable/base_logic/algebra.v
- tests/heapprop.v 17 additions, 20 deletionstests/heapprop.v
- tests/heapprop_affine.ref 0 additions, 0 deletionstests/heapprop_affine.ref
- tests/heapprop_affine.v 261 additions, 0 deletionstests/heapprop_affine.v
- tests/monotone.ref 8 additions, 0 deletionstests/monotone.ref
- tests/monotone.v 16 additions, 0 deletionstests/monotone.v
tests/heapprop_affine.ref
0 → 100644
tests/heapprop_affine.v
0 → 100644
tests/monotone.ref
0 → 100644
tests/monotone.v
0 → 100644