make Prop-level BI connectives notation for bi_emp_valid (rather than bi_entails)
Showing
- iris/base_logic/lib/boxes.v 1 addition, 1 deletioniris/base_logic/lib/boxes.v
- iris/base_logic/lib/gen_inv_heap.v 1 addition, 1 deletioniris/base_logic/lib/gen_inv_heap.v
- iris/base_logic/lib/ghost_map.v 5 additions, 5 deletionsiris/base_logic/lib/ghost_map.v
- iris/base_logic/lib/gset_bij.v 1 addition, 1 deletioniris/base_logic/lib/gset_bij.v
- iris/base_logic/lib/later_credits.v 12 additions, 12 deletionsiris/base_logic/lib/later_credits.v
- iris/base_logic/lib/mono_nat.v 2 additions, 2 deletionsiris/base_logic/lib/mono_nat.v
- iris/base_logic/lib/na_invariants.v 1 addition, 1 deletioniris/base_logic/lib/na_invariants.v
- iris/base_logic/lib/own.v 12 additions, 10 deletionsiris/base_logic/lib/own.v
- iris/base_logic/lib/saved_prop.v 1 addition, 1 deletioniris/base_logic/lib/saved_prop.v
- iris/bi/big_op.v 61 additions, 59 deletionsiris/bi/big_op.v
- iris/bi/derived_laws.v 4 additions, 4 deletionsiris/bi/derived_laws.v
- iris/bi/interface.v 14 additions, 14 deletionsiris/bi/interface.v
- iris/bi/lib/atomic.v 3 additions, 3 deletionsiris/bi/lib/atomic.v
- iris/bi/lib/fractional.v 8 additions, 5 deletionsiris/bi/lib/fractional.v
- iris/bi/lib/laterable.v 8 additions, 8 deletionsiris/bi/lib/laterable.v
- iris/bi/lib/relations.v 2 additions, 2 deletionsiris/bi/lib/relations.v
- iris/bi/monpred.v 4 additions, 4 deletionsiris/bi/monpred.v
- iris/bi/plainly.v 3 additions, 3 deletionsiris/bi/plainly.v
- iris/bi/updates.v 55 additions, 54 deletionsiris/bi/updates.v
- iris/program_logic/lifting.v 1 addition, 1 deletioniris/program_logic/lifting.v
Loading
Please register or sign in to comment