-
- Downloads
get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays
Showing
- iris/algebra/big_op.v 159 additions, 2 deletionsiris/algebra/big_op.v
- iris/algebra/list.v 18 additions, 1 deletioniris/algebra/list.v
- iris/bi/big_op.v 130 additions, 0 deletionsiris/bi/big_op.v
- iris/bi/notation.v 3 additions, 0 deletionsiris/bi/notation.v
- iris/prelude/prelude.v 0 additions, 3 deletionsiris/prelude/prelude.v
- iris_heap_lang/derived_laws.v 170 additions, 70 deletionsiris_heap_lang/derived_laws.v
- iris_heap_lang/lang.v 18 additions, 15 deletionsiris_heap_lang/lang.v
- iris_heap_lang/lib/arith.v 4 additions, 4 deletionsiris_heap_lang/lib/arith.v
- iris_heap_lang/lib/array.v 57 additions, 49 deletionsiris_heap_lang/lib/array.v
- iris_heap_lang/lib/counter.v 5 additions, 5 deletionsiris_heap_lang/lib/counter.v
- iris_heap_lang/lib/ticket_lock.v 3 additions, 3 deletionsiris_heap_lang/lib/ticket_lock.v
- iris_heap_lang/metatheory.v 3 additions, 3 deletionsiris_heap_lang/metatheory.v
- iris_heap_lang/primitive_laws.v 58 additions, 26 deletionsiris_heap_lang/primitive_laws.v
- iris_unstable/heap_lang/interpreter.v 2 additions, 2 deletionsiris_unstable/heap_lang/interpreter.v
- tests/bi.ref 3 additions, 3 deletionstests/bi.ref
- tests/bi.v 11 additions, 11 deletionstests/bi.v
- tests/heap_lang.v 6 additions, 6 deletionstests/heap_lang.v
- tests/ipm_paper.ref 4 additions, 3 deletionstests/ipm_paper.ref
- tests/ipm_paper.v 2 additions, 2 deletionstests/ipm_paper.v
- tests/later_credits_paper.v 5 additions, 3 deletionstests/later_credits_paper.v
Loading
Please register or sign in to comment