Add derived ≼ connective on the BI level.
Showing
- _CoqProject 1 addition, 0 deletions_CoqProject
- iris/algebra/cmra.v 5 additions, 1 deletioniris/algebra/cmra.v
- iris/algebra/csum.v 4 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 4 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 42 additions, 0 deletionsiris/bi/internal_eq.v
- iris/bi/lib/cmra.v 137 additions, 0 deletionsiris/bi/lib/cmra.v
Loading
Please register or sign in to comment