Merge branch 'robbert/bi_persistently_mixin' into 'master'
Show that for non-step indexed BIs, <pers> can trivially be inhabited. See merge request iris/iris!925
No related branches found
No related tags found
Showing
- CHANGELOG.md 4 additions, 0 deletionsCHANGELOG.md
- iris/base_logic/bi.v 12 additions, 4 deletionsiris/base_logic/bi.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
- 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
Loading
Please register or sign in to comment