Skip to content
Snippets Groups Projects
Commit a1d0c311 authored by Marijn van Wezel's avatar Marijn van Wezel
Browse files

Remove superfluous type hints

parent bb981de3
Branches
Tags
1 merge request!577Add `gmultiset_map` and associated lemmas
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
stdpp/gmultiset.v
+ 2
− 2
View file @ a1d0c311
...@@ -783,7 +783,7 @@ Section map. ...@@ -783,7 +783,7 @@ Section map.
Implicit Type f : A -> B. Implicit Type f : A -> B.
Definition gmultiset_map (f : A → B) (X : gmultiset A) : gmultiset B := Definition gmultiset_map f (X : gmultiset A) : gmultiset B :=
list_to_set_disj (f <$> elements X). list_to_set_disj (f <$> elements X).
Lemma elem_of_gmultiset_map f X y : Lemma elem_of_gmultiset_map f X y :
...@@ -824,7 +824,7 @@ Section map. ...@@ -824,7 +824,7 @@ Section map.
Qed. Qed.
Global Instance set_unfold_gmultiset_map Global Instance set_unfold_gmultiset_map
(f : A → B) (X : gmultiset A) (P : A → Prop) y : f X (P : A → Prop) y :
(∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x X (P x)) →
SetUnfoldElemOf y (gmultiset_map f X) (∃ x, y = f x ∧ P x). SetUnfoldElemOf y (gmultiset_map f X) (∃ x, y = f x ∧ P x).
Proof. constructor. rewrite elem_of_gmultiset_map; naive_solver. Qed. Proof. constructor. rewrite elem_of_gmultiset_map; naive_solver. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment