From 6be1cdd22739c0c315ea889aa8c0f0bda87da16d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Mar 2021 20:17:53 +0100
Subject: [PATCH] more exist destruct test cases

---
 tests/proofmode.v | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index bb095de55..9628ea7e4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -457,11 +457,21 @@ Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
 
 (* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
 pure. *)
-Lemma test_pure_and_sep_destruct `{!BiAffine PROP} (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) (P : PROP) :
   ⌜φ⌝ ∧ (⌜φ⌝ ∗ P) -∗ P.
 Proof.
   iIntros "[% [% $]]".
 Qed.
+Lemma test_pure_and_sep_destruct_1 (φ : Prop) (P : PROP) :
+  ⌜φ⌝ ∧ (<affine> ⌜φ⌝ ∗ P) -∗ P.
+Proof.
+  iIntros "[% [% $]]".
+Qed.
+Lemma test_pure_and_sep_destruct_2 (φ : Prop) (P : PROP) :
+  ⌜φ⌝ ∧ (⌜φ⌝ ∗ <absorb> P) -∗ <absorb> P.
+Proof.
+  iIntros "[% [% $]]".
+Qed.
 (* Ensure that [% %] also works when the conjunction is *inside* ⌜...⌝ *)
 Lemma test_pure_inner_and_destruct :
   ⌜False ∧ True⌝ ⊢@{PROP} False.
-- 
GitLab