Commit aa7871c7 authored by Robbert Krebbers's avatar Robbert Krebbers

Test cases for iStopProof.

parent 87729375
......@@ -433,6 +433,11 @@ Tactic failure: iFrame: cannot frame Q.
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
"iStopProof_not_proofmode"
: string
The command has indeed failed with message:
Ltac call to "iStopProof" failed.
Tactic failure: iStopProof: proofmode not started.
"iAlways_spatial_non_empty"
: string
The command has indeed failed with message:
......
......@@ -44,6 +44,9 @@ Definition bar : PROP := (∀ P, foo P)%I.
Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
Lemma test_iStopProof Q : emp - Q - Q.
Proof. iIntros "#H1 H2". iStopProof. by rewrite bi.sep_elim_r. Qed.
Lemma test_iRewrite {A : ofeT} (x y : A) P :
( z, P - <affine> (z y)) - (P - P (x,x) (y,x)).
Proof.
......@@ -765,6 +768,10 @@ Section error_tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Check "iStopProof_not_proofmode".
Lemma iStopProof_not_proofmode : 10 = 10.
Proof. Fail iStopProof. Abort.
Check "iAlways_spatial_non_empty".
Lemma iAlways_spatial_non_empty P :
P - emp.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment