aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tuple.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/Tuple.v')
-rw-r--r--src/Util/Tuple.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 7af4dfe96..7367b1460 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -136,6 +136,13 @@ Definition on_tuple {A B} (f:list A -> list B)
Definition map {n A B} (f:A -> B) (xs:tuple A n) : tuple B n
:= on_tuple (List.map f) (fun _ => eq_trans (map_length _ _)) xs.
+Lemma map_S {n A B} (f:A -> B) (xs:tuple' A n) (x:A)
+ : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x).
+Proof.
+ unfold map, on_tuple.
+ simpl @List.map.
+Admitted.
+
Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat}
(Hlength : forall la lb, length la = a -> length lb = b -> length (f la lb) = c)
(ta:tuple A a) (tb:tuple B b) : tuple C c