- The class `Infinite A` is now defined as having a function
`fresh : list A → A`, that given a list `xs`, gives an element `x ∉ xs`.
- For most types this `fresh` function has a sensible computable behavior,
for example:
+ For numbers, it yields one added to the maximal element in `xs`.
+ For strings, it yields the first string representation of a number that is
not in `xs`.
- For any type `C` of finite sets with elements of infinite type `A`, we lift
the fresh function to `C → A`.
As a consequence:
- It is now possible to pick fresh elements from _any_ finite set and from
_any_ list with elements of an infinite type. Before it was only possible
for specific finite sets, e.g. `gset`, `pset`, ...
- It makes the code more uniform. There was a lot of overlap between having a
`Fresh` and an `Infinite` instance. This got unified.