Merge branch 'non-expansive-notation' into 'master'
notation for declaring a function non-expansive See merge request !42
No related branches found
No related tags found
Showing
- theories/algebra/agree.v 9 additions, 9 deletionstheories/algebra/agree.v
- theories/algebra/auth.v 5 additions, 5 deletionstheories/algebra/auth.v
- theories/algebra/cmra.v 19 additions, 19 deletionstheories/algebra/cmra.v
- theories/algebra/cmra_big_op.v 2 additions, 2 deletionstheories/algebra/cmra_big_op.v
- theories/algebra/cofe_solver.v 5 additions, 5 deletionstheories/algebra/cofe_solver.v
- theories/algebra/csum.v 6 additions, 6 deletionstheories/algebra/csum.v
- theories/algebra/excl.v 4 additions, 4 deletionstheories/algebra/excl.v
- theories/algebra/gmap.v 14 additions, 14 deletionstheories/algebra/gmap.v
- theories/algebra/iprod.v 9 additions, 9 deletionstheories/algebra/iprod.v
- theories/algebra/list.v 27 additions, 27 deletionstheories/algebra/list.v
- theories/algebra/ofe.v 41 additions, 39 deletionstheories/algebra/ofe.v
- theories/algebra/vector.v 5 additions, 5 deletionstheories/algebra/vector.v
- theories/base_logic/derived.v 4 additions, 4 deletionstheories/base_logic/derived.v
- theories/base_logic/double_negation.v 2 additions, 2 deletionstheories/base_logic/double_negation.v
- theories/base_logic/lib/auth.v 1 addition, 1 deletiontheories/base_logic/lib/auth.v
- theories/base_logic/lib/boxes.v 4 additions, 4 deletionstheories/base_logic/lib/boxes.v
- theories/base_logic/lib/cancelable_invariants.v 1 addition, 1 deletiontheories/base_logic/lib/cancelable_invariants.v
- theories/base_logic/lib/fancy_updates.v 1 addition, 1 deletiontheories/base_logic/lib/fancy_updates.v
- theories/base_logic/lib/na_invariants.v 1 addition, 1 deletiontheories/base_logic/lib/na_invariants.v
- theories/base_logic/lib/own.v 4 additions, 4 deletionstheories/base_logic/lib/own.v
Loading
Please register or sign in to comment