Commit b958d569 authored by Ralf Jung's avatar Ralf Jung

test output of iStopProof

parent aa7871c7
Pipeline #19875 failed with stage
in 0 seconds
......@@ -21,6 +21,25 @@
--------------------------------------□
Q ∨ P
"test_iStopProof"
: string
1 subgoal
PROP : sbi
Q : PROP
============================
"H1" : emp
--------------------------------------□
"H2" : Q
--------------------------------------∗
Q
1 subgoal
PROP : sbi
Q : PROP
============================
□ emp ∗ Q -∗ Q
"test_iDestruct_and_emp"
: string
1 subgoal
......
......@@ -44,8 +44,9 @@ Definition bar : PROP := (∀ P, foo P)%I.
Lemma test_unfold_constants : bar.
Proof. iIntros (P) "HP //". Qed.
Check "test_iStopProof".
Lemma test_iStopProof Q : emp - Q - Q.
Proof. iIntros "#H1 H2". iStopProof. by rewrite bi.sep_elim_r. Qed.
Proof. iIntros "#H1 H2". Show. iStopProof. Show. 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)).
......
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