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 169
    • Issues 169
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • 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
  • #330
Closed
Open
Issue created Jun 25, 2020 by Paolo G. Giarrusso@BlaisorbladeContributor

Consider adding `iEnough` variants of `iAssert` ?

Something like:

  Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
    iAssert Q with Hs as pat; first last.
  Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
    iAssert Q as pat; first last.

The point is just readability, and adding all the overloads is probably not worth it, but maybe this would change with an Ltac2 proofmode?

Assignee
Assign to
Time tracking