Skip to content

heap_lang: Make binary "=" operator partial, to sync with CmpXchg

Ralf Jung requested to merge ralf/eq into master

This also gets rid of [val_for_compare]-normalization; instead we introduce a [LitErased] literal that is suited for use by erasure theorems.

Fixes #248 (closed)

Merge request reports