1. 23 Apr, 2019 3 commits
  2. 19 Apr, 2019 2 commits
  3. 26 Mar, 2019 3 commits
  4. 16 Mar, 2019 3 commits
  5. 15 Mar, 2019 5 commits
  6. 14 Mar, 2019 6 commits
  7. 06 Mar, 2019 1 commit
  8. 04 Mar, 2019 1 commit
  9. 03 Mar, 2019 3 commits
    • Robbert's avatar
      Merge branch 'robbert/infinite' into 'master' · 7b80dd85
      Robbert authored
      Overhaul of the `Infinite`/`Fresh` infrastructure
      
      See merge request !58
      7b80dd85
    • Robbert Krebbers's avatar
    • 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
  10. 01 Mar, 2019 4 commits
  11. 28 Feb, 2019 2 commits
  12. 23 Feb, 2019 4 commits
  13. 22 Feb, 2019 1 commit
  14. 21 Feb, 2019 2 commits