Skip to content

GitLab

Merged
Opened by Robbert Krebbers@robbertkrebbersMaintainer

Move HeapLang class instances and tactics to separate file

  • 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