Closed wchargin closed 3 years ago
The nat ref ∧ pos ref cell should be initialized to hold 1 (or any other pos), not 0, so that it's a valid pos ref.
nat ref ∧ pos ref
1
pos
0
pos ref
wchargin-branch: intersecting-references-pos-init
Hah, thanks, nice catch. (For the record, the mistake wasn't present in the Davies & Pfenning paper, I typo'd it when copying it out)
The
nat ref ∧ pos ref
cell should be initialized to hold1
(or any otherpos
), not0
, so that it's a validpos ref
.wchargin-branch: intersecting-references-pos-init