On 30/01/14 11:03, David Matthews wrote:
...
The only safe way to maintain identity of cells is to use a counter or a
ref. An alternative to a ref is to use a locally generated exception
and this may be more efficient than a ref. As a work-around to avoid
the problem with duplication in the
What semantics, if any, does PolyML.pointerEq have? In particular, is
it supposed to be guaranteed that if pointerEq (x,y) is true, then it
will remain true after GC?
My reason for asking is that I've been having trouble with assertion
failures in HOL when reducing large terms. The
