heap_lang: Make binary "=" operator partial, to sync with CmpXchg
This also gets rid of [val_for_compare]-normalization; instead we introduce a [LitErased] literal that is suited for use by erasure theorems.
Showing
- tests/heap_lang.v 3 additions, 2 deletionstests/heap_lang.v
- theories/heap_lang/lang.v 36 additions, 33 deletionstheories/heap_lang/lang.v
- theories/heap_lang/lib/atomic_heap.v 7 additions, 7 deletionstheories/heap_lang/lib/atomic_heap.v
- theories/heap_lang/lifting.v 26 additions, 15 deletionstheories/heap_lang/lifting.v
- theories/heap_lang/proofmode.v 25 additions, 25 deletionstheories/heap_lang/proofmode.v
Loading
Please register or sign in to comment