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 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 15
    • Merge requests 15
  • 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
  • Merge requests
  • !479

Use user-supplied names when destructing existentials with ? intro pattern

  • Review changes

  • Download
  • Email patches
  • Plain diff
Merged Tej Chajed requested to merge tchajed/iris-coq:exists-auto-name into master Jul 18, 2020
  • Overview 64
  • Commits 16
  • Pipelines 0
  • Changes 14

When running iDestruct "H" as (?) "H", use the name of the binder in "H". For example, if "H" has type ∃ y, Φ y, we now use y as the name of the variable after freshening. Previously the name was always the equivalent of running fresh H.

The implementation achieves this by forwarding the desired identifier name through the IntoExist typeclass. Identifiers are serialized in Gallina by using them as the name of a function of type ident_name := unit -> unit.

Edited Jul 20, 2020 by Tej Chajed
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: exists-auto-name