diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-06 17:05:55 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-06 17:05:55 -0500 |
commit | 12d083871316497a1743b0fbac14514d39996aeb (patch) | |
tree | f559e3444de4b1a07ffef1bfdd1424f40cd72816 /src/Util | |
parent | beaf8c386549f99d0366f7c6a269ebb9ce311c5f (diff) |
Add Tuple.map_map2 (admitted)
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Tuple.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 7367b1460..554f9e14e 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -152,6 +152,11 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys. +Lemma map_map2 {n A B C D} (f:A -> B -> C) (g:C -> D) (xs:tuple A n) (ys:tuple B n) + : map g (map2 f xs ys) = map2 (fun a b => g (f a b)) xs ys. +Proof. +Admitted. + Section monad. Context (M : Type -> Type) (bind : forall X Y, M X -> (X -> M Y) -> M Y) (ret : forall X, X -> M X). Fixpoint lift_monad' {n A} {struct n} |