From 8e1e9c0303b29d064bd51dc6cb991b1e2255881f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jul 2022 09:27:54 +0200
Subject: [PATCH] Add tests.

---
 tests/proofmode_iris.ref | 32 ++++++++++++++++++++++++++++++++
 tests/proofmode_iris.v   |  9 +++++++++
 2 files changed, 41 insertions(+)

diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 4c4d3a96c..229402b79 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -172,6 +172,38 @@ Tactic failure: iInv: invariant "H2" not found.
      : string
 The command has indeed failed with message:
 Tactic failure: iMod: "H" not fresh.
+"test_iIntros_lc"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  invGS0 : invGS Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  n, m : nat
+  ============================
+  "Hlc1" : £ (S n)
+  "Hlc2" : £ m
+  --------------------------------------∗
+  £ (S n)
+"lc_iSplit_lc"
+     : string
+2 goals
+  
+  Σ : gFunctors
+  invGS0 : invGS Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  n, m : nat
+  ============================
+  "Hlc1" : £ (S n)
+  --------------------------------------∗
+  £ (S n)
+
+goal 2 is:
+ "Hlc2" : £ m
+ --------------------------------------∗
+ £ m
 "test_iInv"
      : string
 1 goal
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 466099cd2..6884d140b 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -250,6 +250,15 @@ Section iris_tests.
     iIntros "H H'". Fail iDestruct "H'" as ">H".
   Abort.
 
+  (** Make sure that the splitting rule for [+] gets priority over the one for
+  [S]. See issue #470. *)
+  Check "test_iIntros_lc".
+  Lemma test_iIntros_lc n m : £ (S n + m) -∗ £ (S n).
+  Proof. iIntros "[Hlc1 Hlc2]". Show. iExact "Hlc1". Qed.
+
+  Check "lc_iSplit_lc".
+  Lemma lc_iSplit_lc n m : £ (S n) -∗ £ m -∗ £ (S n + m).
+  Proof. iIntros "Hlc1 Hlc2". iSplitL "Hlc1". Show. all: done. Qed.
 End iris_tests.
 
 Section monpred_tests.
-- 
GitLab