From f7255e634e4d548b6c50152969daa8cdcf87fcb7 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 9 Aug 2022 16:11:15 +0200 Subject: [PATCH] Add test. --- tests/proofmode.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/proofmode.v b/tests/proofmode.v index 963f2986a..ea515a6b8 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -325,6 +325,10 @@ Definition tc_opaque_test : PROP := tc_opaque (∀ x : nat, ⌜ x = x âŒ)%I. Lemma test_iIntros_tc_opaque : ⊢ tc_opaque_test. Proof. by iIntros (x). Qed. +Definition tc_opaque_test_sep : PROP := tc_opaque (emp ∗ emp)%I. +Lemma test_iDestruct_tc_opaque_sep : tc_opaque_test_sep -∗ tc_opaque_test_sep. +Proof. iIntros "[H1 H2]". by iSplitL. Qed. + Lemma test_iApply_evar P Q R : (∀ Q, Q -∗ P) -∗ R -∗ P. Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed. -- GitLab