From 8daabbfc59a93d66494853ffdf9039a2d1a5b645 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Apr 2021 23:55:57 +0200
Subject: [PATCH] Add pretty printing tests for multiset literals.

---
 tests/notation.ref |  9 +++++++++
 tests/notation.v   | 16 +++++++++++++++-
 2 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/tests/notation.ref b/tests/notation.ref
index 026cb4d4..4d53c67c 100644
--- a/tests/notation.ref
+++ b/tests/notation.ref
@@ -24,3 +24,12 @@ test_op_4 =
   4 := {[4 := [4]]};
   5 := {[5 := [5]]}]}
      : M (M (list nat))
+test_gmultiset_1 = {[+ 10 +]}
+     : gmultiset nat
+test_gmultiset_2 = {[+ 10; 11 +]}
+     : gmultiset nat
+test_gmultiset_3 = {[+ 10; 11; 2 - 2 +]}
+     : gmultiset nat
+test_gmultiset_4 = 
+{[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}
+     : gmultiset (gmultiset nat)
diff --git a/tests/notation.v b/tests/notation.v
index 467f1952..41fe94e9 100644
--- a/tests/notation.v
+++ b/tests/notation.v
@@ -1,4 +1,4 @@
-From stdpp Require Import base tactics fin_maps.
+From stdpp Require Import base tactics fin_maps gmultiset.
 
 (** Test parsing of variants of [(≡)] notation. *)
 Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
@@ -35,3 +35,17 @@ Section map_notations.
   Print test_op_3.
   Print test_op_4.
 End map_notations.
+
+(** Test that notations for maps with multiple elements can be parsed and printed correctly. *)
+Section multiset_notations.
+  Definition test_gmultiset_1 : gmultiset nat := {[+ 10 +]}.
+  Definition test_gmultiset_2 : gmultiset nat := {[+ 10; 11 +]}.
+  Definition test_gmultiset_3 : gmultiset nat := {[+ 10; 11; 2 - 2 +]}.
+  Definition test_gmultiset_4 : gmultiset (gmultiset nat) :=
+    {[+ {[+ 10 +]}; ∅; {[+ 2 - 2; 10 +]} +]}.
+
+  Print test_gmultiset_1.
+  Print test_gmultiset_2.
+  Print test_gmultiset_3.
+  Print test_gmultiset_4.
+End multiset_notations.
\ No newline at end of file
-- 
GitLab