From 037f7e3fc0a90c9bec509ab468949ad60f08f59d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Feb 2018 22:55:49 +0100
Subject: [PATCH] Test cases for issue #148.

---
 theories/tests/proofmode.v | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 660d174cb..97d711b50 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -291,12 +291,17 @@ Proof.
   iSpecialize ("HÏ†" with "[% //] HP"). done.
 Qed.
 
-Lemma test_iNext_laterN_later P n : â–· â–·^n P âŠ¢ â–·^n â–· P.
+Lemma test_iNext_laterN_later P n : â–· â–·^n P -âˆ— â–·^n â–· P.
 Proof. iIntros "H". iNext. by iNext. Qed.
-Lemma test_iNext_later_laterN P n : â–·^n â–· P âŠ¢ â–· â–·^n P.
+Lemma test_iNext_later_laterN P n : â–·^n â–· P -âˆ— â–· â–·^n P.
 Proof. iIntros "H". iNext. by iNext. Qed.
-Lemma test_iNext_laterN_laterN P n1 n2 : â–· â–·^n1 â–·^n2 P âŠ¢ â–·^n1 â–·^n2 â–· P.
+Lemma test_iNext_plus_1 P n1 n2 : â–· â–·^n1 â–·^n2 P -âˆ— â–·^n1 â–·^n2 â–· P.
 Proof. iIntros "H". iNext. iNext. by iNext. Qed.
+Lemma test_iNext_plus_2 P n m : â–·^n â–·^m P -âˆ— â–·^(n+m) P.
+Proof. iIntros "H". iNext. done. Qed.
+Lemma test_iNext_plus_3 P Q n m k :
+  â–·^m â–·^(2 + S n + k) P -âˆ— â–·^m â–· â–·^(2 + S n) Q -âˆ— â–·^k â–· â–·^(S (S n + S m)) (P âˆ— Q).
+Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
 
 Lemma test_iEval x y : âŒœ (y + x)%nat = 1 âŒ -âˆ— âŒœ S (x + y) = 2%nat âŒ : uPred M.
 Proof.
-- 
GitLab