git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2957 from david-christiansen/issue/2956
fab2fe0David Christiansen
libs/base/Data/Vect.idr+6−2
compare with master
unifiedsplit
@@ -198,8 +198,12 @@ replicate (S k) x = x :: replicate k x
198-- Zips and unzips
198-- Zips and unzips
199--------------------------------------------------------------------------------
199--------------------------------------------------------------------------------
200
200
201−||| Combine two equal-length vectors pairwise with some function
201+||| Combine two equal-length vectors pairwise with some function.
202+|||
203+||| @ f the function to combine elements with
204+||| @ xs the first vector of elements
205+||| @ ys the second vector of elements
202−zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
206+zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
203zipWith f [] [] = []
207zipWith f [] [] = []
204zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
208zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
205
209
libs/prelude/Prelude/Stream.idr+6−2
@@ -62,8 +62,12 @@ index : Nat -> Stream a -> a
62index Z (x::xs) = x
62index Z (x::xs) = x
63index (S k) (x::xs) = index k xs
63index (S k) (x::xs) = index k xs
64
64
65−||| Combine two streams element-wise using a function
65+||| Combine two streams element-wise using a function.
66+|||
67+||| @ f the function to combine elements with
68+||| @ xs the first stream of elements
69+||| @ ys the second stream of elements
66−zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
70+zipWith : (f : a -> b -> c) -> (xs : Stream a) -> (ys : Stream b) -> Stream c
67zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
71zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
68
72
69||| Combine three streams by applying a function element-wise along them
73||| Combine three streams by applying a function element-wise along them