From 63835cb3c94c0808d008354991a9eec276de0cbc Mon Sep 17 00:00:00 2001
From: Marijn van Wezel <marijn@wikibase.nl>
Date: Thu, 17 Oct 2024 15:45:32 +0200
Subject: [PATCH] Move definition to top
---
stdpp/gmultiset.v | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/stdpp/gmultiset.v b/stdpp/gmultiset.v
index 6cf5d940..4e2e529b 100644
--- a/stdpp/gmultiset.v
+++ b/stdpp/gmultiset.v
@@ -63,6 +63,13 @@ Section definitions.
let (X) := X in dom X.
End definitions.
+Section more_definitions.
+ Context `{Countable A} `{Countable B}.
+
+ Definition gmultiset_map f (X : gmultiset A) : gmultiset B :=
+ list_to_set_disj (f <$> elements X).
+End more_definitions.
+
Global Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
Global Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
Global Typeclasses Opaque gmultiset_singleton gmultiset_union gmultiset_difference.
@@ -783,9 +790,6 @@ Section map.
Implicit Type f : A → B.
- Definition gmultiset_map f (X : gmultiset A) : gmultiset B :=
- list_to_set_disj (f <$> elements X).
-
Lemma elem_of_gmultiset_map f X y :
y ∈ gmultiset_map f X ↔ ∃ x, y = f x ∧ x ∈ X.
Proof.
--
GitLab