Skip to content
GitLab
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 170
    • Issues 170
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 23
    • Merge requests 23
  • 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
  • IrisIris
  • Issues
  • #64
Closed
Open
Issue created Jan 10, 2017 by Ralf Jung@jungOwner

Destruct patterns: Support -> and <- (at least) for pure Coq equalities, and maybe injection patterns

In lambdaRust, we sometimes write something like iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %->. It would be nice if we could write iDestruct "H" as "[? ->]".

As a bonus: We also even more often write iDestruct "H" as "[? EQ]"; iDestruct "EQ" as %[= ->], i.e., there is an additional injection applied. Any way we could also get that in the proof mode? Maybe even using the "injective" typeclass so that it doesn't have to be the constructor of an inductive type (however, of course it'd also have to support all constructors, so it can't rely just on that typeclass).

Assignee
Assign to
Time tracking