4.2. The HeapLang Interpreter (Optional)🔗

The Rocq port of Iris ships a rudimentary HeapLang interpreter in iris.unstable.heap_lang. At the time of this writing, iris-lean does not include an interpreter, so the Compute (exec ...) incantations that appear in the Rocq tutorial cannot be run directly in Lean. We still see, however, that HeapLang expressions are pieces of syntax we can inspect with #check.

TODO (upstream — iris-lean): once an exec evaluator lands, restore the #eval exec 10 ... lines that the Rocq tutorial uses to display runtime values for each example below.