Permalink
Browse files

Normalized type for Vector.map2

fix CoRN but there must be an underlying bug ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16355 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent 6191ae4 commit 39f62b3ecf3e5dcadd16b10a81c495a30bd24251 @pirbo pirbo committed Mar 25, 2013
Showing with 2 additions and 1 deletion.
  1. +2 −1 theories/Vectors/VectorDef.v
@@ -212,7 +212,8 @@ Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n :=
end.
(** map2 g [x1 .. xn] [y1 .. yn] = [(g x1 y1) .. (g xn yn)] *)
-Definition map2 {A B C} (g:A -> B -> C) :=
+Definition map2 {A B C} (g:A -> B -> C) :
+ forall (n : nat), t A n -> t B n -> t C n :=
@rect2 _ _ (fun n _ _ => t C n) (nil C) (fun _ _ _ H a b => (g a b) :: H).
Global Arguments map2 {A B C} g {n} v1 v2.

0 comments on commit 39f62b3

Please sign in to comment.