Seal HeapLang points-to
HeapLang defines a notation for the gen_heap
points-to. This notation has two purposes (1) use Some
for the value and (2) fix the arguments to the HeapLang val
so that type inference and scopes work better.
It's currently quite easy to accidentally break abstraction. It's also easy to forget to lift a gen_heap
lemma because it might work accidentally for the notation.
We thus should make the HeapLang points-to a definition and seal it.
See also the discussion in !960 (comment 98626)