Skip to content

WIP: Prepend introduction pattern `H.ipat`.

Robbert Krebbers requested to merge robbert/prepend into master

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

Merge request reports