Skip to content

GitLab

I
Iris
Open
Opened 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?