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 81
    • Issues 81
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 12
    • Merge requests 12
  • 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
  • !407

Generalize Propers for lists / Add some missing Params

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/list_proper into master Aug 10, 2022
  • Overview 4
  • Commits 4
  • Pipelines 2
  • Changes 3

For example, for fmap:

  • Old: Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f)
  • New: Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap

This means that solve_proper can also find a Proper instance when the two functions are different, and then prove that they are extensionally equal.

This is similar to what we have done in !276 (merged) for maps.

Edited Aug 10, 2022 by Ralf Jung
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: robbert/list_proper