This PR features a new design of identType.
We require identType to be an infinite countable type.
This decision gives us fresh, fresh_seq, and other related functions almost for free.
Another nice thing is that we have canonical total well-founded order on identifiers induced by countability.
A description of the reworked interface of identType can be found in the docs at the top of ident.v
This PR features a new design of
identType. We requireidentTypeto be an infinite countable type. This decision gives usfresh,fresh_seq, and other related functions almost for free. Another nice thing is that we have canonical total well-founded order on identifiers induced by countability.A description of the reworked interface of
identTypecan be found in the docs at the top ofident.v