Skip to content

Clean up \valForm / \exprForm

Jonas Kastberg requested to merge jihgfee/iris-coq:heaplang-form-cleanup into master

The heaplang.sty file contains three separate macros for \Rec, to support the expression and value forms of the construct. However, this is inconsistent with the similar pattern for inl and inr, that similarly uses the forms, but do not have corresponding macros.

In the intent of keeping the heaplang.sty file condensed, this MR suggests to remove the specific \Rec constructs, and instead inline them when used. This is inline with the intention that these explicit annotations are supposed to be used sparingly.

Additionally, this MR proposes to move the annotations in the inl/inr constructs to be on the operator, rather than the argument, as this is more consistent with the annotations on \Rec. That is, inl_e(arg) as opposed to inl(arg)_e.

Merge request reports