Overhaul of the `Infinite`/`Fresh` infrastructure
Overhaul of the Infinite
/Fresh
infrastructure.
- The class
Infinite A
is now defined as having a functionfresh : list A → A
, that given a listxs
, gives an elementx ∉ 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 numbers, it yields one added to the maximal element in
- For any type
C
of finite sets with elements of infinite typeA
, we lift the fresh function toC → 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 anInfinite
instance. This got unified.