WIP: Prepend introduction pattern `H.ipat`.
The new introduction pattern H.ipat
prepends the name H
to all names appearing in ipat
.
For example:
Lemma test_iDestruct_prepend_1 P Q :
P ∗ Q -∗ Q ∗ P.
Proof. iIntros "H.[P Q]".
This will give hypotheses HP
and HQ
.
This feature will be particularly useful with the record-like syntax that @tchajed @jtassaro @jung and me are working on.
TODO
-
Bikeshed about the syntax. The period .
may cause annoyances with the electric terminator in Emacs?
Edited by Ralf Jung