From bfe7dd4c44d609088acadf40e1be500f76388a73 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 May 2017 16:21:39 +0200
Subject: [PATCH] =?UTF-8?q?Add=20test=20for=20iL=C3=B6b.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/tests/proofmode.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index d4584baae..c162461d7 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -162,6 +162,12 @@ Proof. iIntros "#?". by iSplit. Qed.
 Lemma test_iSpecialize_persistent P Q :
   □ P -∗ (□ P -∗ Q) -∗ Q.
 Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
+
+Lemma test_iLöb P : (∃ n, ▷^n P)%I.
+Proof.
+  iLöb as "IH". iDestruct "IH" as (n) "IH".
+  by iExists (S n).
+Qed.
 End tests.
 
 Section more_tests.
-- 
GitLab