Skip to content

GitLab

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

Merged
Opened Jul 18, 2020 by Tej Chajed@tchajedDeveloper

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

  • Overview 64
  • Commits 16
  • 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
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Reference: iris/iris!479
Source branch: exists-auto-name