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 123
    • Issues 123
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 14
    • Merge Requests 14
  • 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
  • !254

Merged
Created May 24, 2019 by Robbert Krebbers@robbertkrebbersMaintainer

Alternative take on making proof mode terms more compact.

  • Overview 12
  • Commits 4
  • Pipelines 6
  • Changes 2

This is an alternative to !224 (closed) by splitting up envs_lookup_delete premises into envs_lookup and envs_delete.

@jtassaro Could you rebase !224 (closed) so we can compare?

The following tactics involve some other tricks:

  • tac_assumption: uses a let binding for envs_delete since its result is used twice
  • tac_specialize: uses a let binding for envs_delete since its result is used twice
  • tac_specialize_assert: uses a conjunction, not sure if it's worth the extra bloat in the Ltac code to do something smarter here.
Edited Jun 05, 2019 by Robbert Krebbers
Assignee
Assign to
Reviewer
Request review from
None
Milestone
None
Assign milestone
Time tracking
Source branch: ci/robbert/pm_faster_alt