Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
S
stdpp
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 47
    • Issues 47
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 3
    • Merge Requests 3
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Iris
  • stdpp
  • Merge Requests
  • !58

Merged
Opened Mar 01, 2019 by Robbert@robbertkrebbersMaintainer

Overhaul of the `Infinite`/`Fresh` infrastructure

  • Overview 30
  • Commits 2
  • 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
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/stdpp!58
Source branch: robbert/infinite

Revert this merge request

This will create a new commit in order to revert the existing changes.

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.

Cherry-pick this merge request

Switch branch
Cancel
A new branch will be created in your fork and a new merge request will be started.