Commit 8f319109 authored by Ralf Jung's avatar Ralf Jung

add an interesting test output

parent 24f054ec
Pipeline #9350 passed with stage
in 27 minutes and 10 seconds
...@@ -19,3 +19,15 @@ ...@@ -19,3 +19,15 @@
--------------------------------------□ --------------------------------------□
Q ∨ P Q ∨ P
1 subgoal
PROP : sbi
P, Q : PROP
Persistent0 : Persistent P
Persistent1 : Persistent Q
============================
_ : P
_ : Q
--------------------------------------□
<affine> (P ∗ Q)
...@@ -54,7 +54,7 @@ Qed. ...@@ -54,7 +54,7 @@ Qed.
Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} : Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
P emp - emp Q - <affine> (P Q). P emp - emp Q - <affine> (P Q).
Proof. iIntros "[#? _] [_ #?]". auto. Qed. Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P Q P Q)%I. Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P Q P Q)%I.
Proof. iIntros "H1 #H2". by iFrame "∗#". Qed. Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
......
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