This module implements a very simple notion of ``mark''.
The type of marks.
fresh() generates a fresh mark, that is, a mark that is guaranteed
to be distinct from all existing marks.
same mark1 mark2 tells whether mark1 and mark2 are the same
mark, that is, were created by the same call to fresh.
same mark1 mark2
none is a distinguished mark, created via an initial call to