Skip to content
GitLab

Move HeapLang class instances and tactics to separate file

Merged Robbert Krebbers requested to merge robbert/heap_lang_tweaks into master
  • Move IntoVal, AsVal, Atomic, AsRecV, and PureExec instances to their own file heap_lang.class_instances
  • Move inv_head_step tactic and head_step instances (now part of new hint database head_step) to heap_lang.tactics

I ported Iron so that it uses Iris's HeapLang instead of forking it. Iron defines its own WP (in a linear rather than affine logic), but should reuse all HeapLang class instances and tactics. Hence, they should not be in primitive_laws.

Edited by Robbert Krebbers