Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 79
    • Issues 79
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 14
    • Merge requests 14
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !58

Overhaul of the `Infinite`/`Fresh` infrastructure

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/infinite into master Mar 01, 2019
  • Overview 30
  • Commits 2
  • Pipelines 0
  • Changes 7

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.
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/infinite