From 8f80353dda8ebcd332471721a0c38a8977f45c47 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Jun 2020 15:10:16 +0200
Subject: [PATCH] Add tests for `multiset_solver`.

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

diff --git a/tests/multiset_solver.ref b/tests/multiset_solver.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
new file mode 100644
index 00000000..a52397cf
--- /dev/null
+++ b/tests/multiset_solver.v
@@ -0,0 +1,18 @@
+From stdpp Require Import gmultiset.
+
+Section test.
+  Context `{Countable A}.
+  Implicit Types x y : A.
+  Implicit Types X Y : gmultiset A.
+
+  Lemma test1 x y X : {[x]} ⊎ ({[y]} ⊎ X) ≠ ∅.
+  Proof. multiset_solver. Qed.
+  Lemma test2 x y X : {[x]} ⊎ ({[y]} ⊎ X) = {[y]} ⊎ ({[x]} ⊎ X).
+  Proof. multiset_solver. Qed.
+  Lemma test3 x : {[x]} ⊎ ∅ ≠@{gmultiset A} ∅.
+  Proof. multiset_solver. Qed.
+  Lemma test4 x y z X Y :
+    {[z]} ⊎ X = {[y]} ⊎ Y →
+    {[x]} ⊎ ({[z]} ⊎ X) = {[y]} ⊎ ({[x]} ⊎ Y).
+  Proof. multiset_solver. Qed.
+End test.
-- 
GitLab