Overhaul of the Infinite
/Fresh
infrastructure.
Infinite A
is now defined as having a function
fresh : list A → A
, that given a list xs
, gives an element x ∉ xs
.fresh
function has a sensible computable behavior,
for example:
xs
.xs
.C
of finite sets with elements of infinite type A
, we lift
the fresh function to C → A
.As a consequence:
gset
, pset
, ...Fresh
and an Infinite
instance. This got unified.