Skip to content
Snippets Groups Projects
Commit 84708e6c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'map_zip_with_swap' into 'master'

Add `map_zip_with_flip`.

See merge request iris/stdpp!88
parents 62966bac 273e12e9
No related branches found
No related tags found
1 merge request!88Add `map_zip_with_flip`.
Pipeline #19310 passed
......@@ -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 (flip f) m2 m1 = map_zip_with f m1 m2.
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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment