Merge branch 'ike/internal_included' into 'master'
Add derived ≼ connective on the BI level. See merge request iris/iris!944
No related branches found
No related tags found
Showing
- CHANGELOG.md 5 additions, 1 deletionCHANGELOG.md
- _CoqProject 1 addition, 0 deletions_CoqProject
- iris/algebra/cmra.v 8 additions, 1 deletioniris/algebra/cmra.v
- iris/algebra/csum.v 7 additions, 0 deletionsiris/algebra/csum.v
- iris/algebra/dyn_reservation_map.v 2 additions, 1 deletioniris/algebra/dyn_reservation_map.v
- iris/algebra/excl.v 7 additions, 0 deletionsiris/algebra/excl.v
- iris/algebra/gmap.v 1 addition, 2 deletionsiris/algebra/gmap.v
- iris/algebra/max_prefix_list.v 1 addition, 1 deletioniris/algebra/max_prefix_list.v
- iris/algebra/reservation_map.v 1 addition, 1 deletioniris/algebra/reservation_map.v
- iris/algebra/view.v 5 additions, 5 deletionsiris/algebra/view.v
- iris/base_logic/algebra.v 2 additions, 32 deletionsiris/base_logic/algebra.v
- iris/bi/internal_eq.v 41 additions, 0 deletionsiris/bi/internal_eq.v
- iris/bi/lib/cmra.v 152 additions, 0 deletionsiris/bi/lib/cmra.v
Loading
Please register or sign in to comment