The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
Missing error message with `iDestruct ... as "#..."`
Testcase:
Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ Q ∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP".Prints
No matching clauses for match.That's never an acceptable error message, obviously.