diff options
author | jadep <jade.philipoom@gmail.com> | 2017-06-26 08:42:33 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2017-06-26 08:43:40 -0400 |
commit | b259663f37d8cf05ad247c1fe3232b08f6e09e8b (patch) | |
tree | bd13c04b7999cb0c32983357345303dd0fa0b390 /src/Util/CPSUtil.v | |
parent | 151df89143db440f11e99127a25b26b02d59f48b (diff) |
remove unused admit (has been moved to Tuple.v)
Diffstat (limited to 'src/Util/CPSUtil.v')
-rw-r--r-- | src/Util/CPSUtil.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index 506cda2e7..e75eda04d 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -276,16 +276,6 @@ Module Tuple. | S n' => fun xs ys T f => map2_cps g (tl xs) (tl ys) (fun zs => f (append (g (hd xs) (hd ys)) zs)) end. - - 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; try reflexivity. - cbn [append]. - rewrite map2_S'. - reflexivity. - Qed. Lemma map2_cps_correct {n A B C} g xs ys : forall {T} f, @map2_cps n A B C g xs ys T f = f (map2 g xs ys). Proof. |