Commit cc95f0fb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Test case for `iAlways` and the `absolutely` modality.

parent 12326eeb
...@@ -67,4 +67,11 @@ Section tests. ...@@ -67,4 +67,11 @@ Section tests.
Proof. Proof.
iIntros "H HP". by iApply "H". iIntros "H HP". by iApply "H".
Qed. Qed.
Lemma test_absolutely P Q : emp - P - Q - (P Q).
Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
Lemma test_absolutely_affine `{BiAffine PROP} P Q R :
emp - P - Q - R - (P Q).
Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
End tests. End tests.
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