The explainer covers the static semantics of the proposed extension, but not so such its dynamic semantics. We do have the reduction rules scattered between an old document and in a comment on another issue. We should bring these together into the execution section of the explainer.