From 39a49468836a334ecf97a9645145cbe0fdda74a1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2022 16:42:17 +0100
Subject: [PATCH] Some tests.

---
 tests/bi.v | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/tests/bi.v b/tests/bi.v
index 87f512560..bab686754 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import bi plainly.
+From iris.bi Require Import bi plainly big_op.
 
 (** See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/610 *)
 Lemma test_impl_persistent_1 `{!BiPlainly PROP, !BiPersistentlyImplPlainly PROP} :
@@ -14,3 +14,26 @@ Proof.
   (* [<affine> True] is implicitly in %I scope. *)
   pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
 Abort.
+
+(** Some basic tests to make sure patterns work in big ops. *)
+Definition big_sepM_pattern_value
+    {PROP : bi} (m : gmap nat (nat * nat)) : PROP :=
+  [∗ map] '(x,y) ∈ m, ⌜ 10 = x ⌝.
+
+Definition big_sepM_pattern_value_tt
+    {PROP : bi} (m : gmap nat ()) : PROP :=
+  [∗ map] '() ∈ m, True.
+
+Definition big_sepM_pattern_key
+    {PROP : bi} (m : gmap (nat * nat) nat) : PROP :=
+  [∗ map] '(k,_) ↦ _ ∈ m, ⌜ 10 = k ⌝.
+
+Definition big_sepM_pattern_both
+    {PROP : bi} (m : gmap (nat * nat) (nat * nat)) : PROP :=
+  [∗ map] '(k,_) ↦ '(_,y) ∈ m, ⌜ k = y ⌝.
+
+Definition big_sepM_cast {PROP : bi} (m : gmap nat nat) : PROP :=
+  [∗ map] (x:nat) ∈ m, ⌜ 10%Z = x ⌝.
+
+Definition big_sepM2_pattern {PROP : bi} (m1 m2 : gmap nat (nat * nat)) : PROP :=
+  [∗ map] '(x,_);'(_,y) ∈ m1;m2, ⌜ x = y ⌝.
\ No newline at end of file
-- 
GitLab