Skip to content

heap_lang lifting: instantiate inv_heapG and inv_heap_inv

Ralf Jung requested to merge ralf/inv_heap into master

This was quite annoying in examples@99f8ad18, to have to explicitly pass loc val all the time.

However, this means that inv_heap will be exported by default into every heap_lang user. I am a bit worried people might accidentally rely on there being a GC in their model. But maybe that's okay?

Merge request reports