Commit f9af00d1 authored by Dan Frumin's avatar Dan Frumin

Add `map_zip_with_flip`.

parent 0b3d1e9f
......@@ -1369,6 +1369,13 @@ Proof.
by destruct (m1 !! i), (m2 !! i).
Qed.
Lemma map_zip_with_flip {A B C} (f : A B C) (m1 : M A) (m2 : M B) :
map_zip_with f m1 m2 = map_zip_with (flip f) m2 m1.
Proof.
apply map_eq; intro i. rewrite !map_lookup_zip_with.
by destruct (m1 !! i), (m2 !! i).
Qed.
Lemma map_zip_with_map_zip {A B C} (f : A B C) (m1 : M A) (m2 : M B) :
map_zip_with f m1 m2 = curry f <$> map_zip m1 m2.
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment