Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 153
    • Issues 153
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 8
    • Merge requests 8
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Merge requests
  • !789

Let `iRevert` of a pure hypotheses generate a wand instead of implication.

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Robbert Krebbers requested to merge robbert/iRevert_pure into master Apr 23, 2022
  • Overview 3
  • Commits 4
  • Pipelines 2
  • Changes 5

Because implications are strange and wands are nicer.

This matches with our general consensus to prefer wand/star over implication/conjunction.

In case the BI is not affine, the wand is weaker than the implication, so we add an affine modality.

Edited Apr 25, 2022 by Robbert Krebbers
Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: robbert/iRevert_pure