From c19c7aa0b4efa8a2529304d4c4e46435d765699e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 10 Nov 2016 14:51:57 -0500 Subject: Add Tuple and HList lemmas --- src/Util/Tuple.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 79747ec2d..d1dcbca30 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -195,6 +195,10 @@ Proof. simpl @List.map. Admitted. +Lemma map_to_list {A B n ts} (f : A -> B) + : List.map f (@to_list A n ts) = @to_list B n (map f ts). +Proof. 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 -- cgit v1.2.3