GitLab

Overhaul of the Infinite/Fresh infrastructure.

• 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.