From eef6260f0ba81e101b98c04568dad6c5d983099c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 6 Feb 2020 18:21:11 +0100
Subject: [PATCH] Add test case.
---
tests/proofmode.v | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 27b0a34e1..b0d52b54c 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -239,6 +239,14 @@ Proof.
iFrame.
Qed.
+Lemma test_iExists_unused : (∃ P : PROP, ∃ x : nat, P)%I.
+Proof.
+ iExists _.
+ iExists 10.
+ iAssert emp%I as "H"; first done.
+ iExact "H".
+Qed.
+
(* Check coercions *)
Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
--
GitLab