diff options
Diffstat (limited to 'src/Util/Tuple.v')
| -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 775c7cb8d..2dbc592ff 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -791,6 +791,11 @@ Lemma map_append {A B n} (f:A->B) : forall (x:tuple A n) (a:A), map f (append a x) = append (f a) (map f x). Proof. destruct n; auto using map_append'. Qed. +Lemma map2_append n A B C f xs ys x y : + @map2 (S n) A B C f (append x xs) (append y ys) + = append (f x y) (map2 f xs ys). +Proof. destruct n; [reflexivity|]. apply map2_S'. Qed. + Fixpoint nth_default {A m} (d:A) n : tuple A m -> A := match m, n with | O, _ => fun _ => d |