diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-25 00:27:12 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-25 00:27:12 +0000 |
| commit | 39f62b3ecf3e5dcadd16b10a81c495a30bd24251 (patch) | |
| tree | 944320fb7c081e6fca87224f783ccd395e5bfbb6 /theories/Vectors | |
| parent | 6191ae4ca4cc99aa9412745abc4991212a5f70d7 (diff) | |
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
Diffstat (limited to 'theories/Vectors')
| -rw-r--r-- | theories/Vectors/VectorDef.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 38675f31e..8f672deda 100644 --- a/theories/Vectors/VectorDef.v +++ b/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. |