From eaca08459b5c89c2c6ad32c3d41f929035c6b0ac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Nov 2022 19:00:45 +0100
Subject: [PATCH] Tests.

---
 tests/gset.ref |  0
 tests/gset.v   | 15 +++++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 tests/gset.ref
 create mode 100644 tests/gset.v

diff --git a/tests/gset.ref b/tests/gset.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/gset.v b/tests/gset.v
new file mode 100644
index 000000000..d84576681
--- /dev/null
+++ b/tests/gset.v
@@ -0,0 +1,15 @@
+From iris.algebra Require Import gset.
+
+Lemma test_op (X Y : gset nat) : X ⊆ Y → X ⋅ Y = Y.
+Proof. set_solver. Qed.
+Lemma test_included (X Y : gset nat) : X ≼ Y → X ∪ Y = Y ∧ X ∩ Y = X.
+Proof. set_solver. Qed.
+
+Lemma test_disj_included (X Y : gset nat) : GSet X ≼ GSet Y → X ∪ Y = Y ∧ X ∩ Y = X.
+Proof. set_solver. Qed.
+Lemma test_disj_equiv n : GSet (∅ : gset nat) ≡ GSet {[n]} → False.
+Proof. set_solver. Qed.
+Lemma test_disj_eq n : GSet (∅ : gset nat) = GSet {[n]} → False.
+Proof. set_solver. Qed.
+Lemma test_disj_valid (X Y : gset nat) : ✓ (GSet X ⋅ GSet Y) → X ∩ Y = ∅.
+Proof. set_solver. Qed.
-- 
GitLab