• Robbert Krebbers's avatar
    Overhaul of the `Infinite`/`Fresh` infrastructure. · 3184ef61
    Robbert Krebbers authored
    - 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.
    3184ef61
nmap.v 3.33 KB