diff --git a/tests/notation.ref b/tests/notation.ref index 026cb4d4e5ddced30371859d4f9504f682bc8522..4d53c67c775137daaf00f3b83ff54b17c83080ef 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 467f1952d55d74f57b84d70d17430bb78dc16053..41fe94e9cea8db3335688669f0386d3c196390a7 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