git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2957 from david-christiansen/issue/2956

Detail in docstring for zipWith on Vect and Stream

commitfab2fe0c4b584ba091cecab7cc533304e7dc4755 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 8 Feb 2016, 19:21 (11 years ago) parent36448f905c0eba
2 files changed+12−4
compare with master
unifiedsplit
libs/base/Data/Vect.idr+6−2 libs/prelude/Prelude/Stream.idr+6−2
libs/base/Data/Vect.idr+6−2
@@ -198,8 +198,12 @@ replicate (S k) x = x :: replicate k x
198198-- Zips and unzips
199199--------------------------------------------------------------------------------
200200
201−||| Combine two equal-length vectors pairwise with some function
202−zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
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
206+zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
203207zipWith f [] [] = []
204208zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
205209
libs/prelude/Prelude/Stream.idr+6−2
@@ -62,8 +62,12 @@ index : Nat -> Stream a -> a
6262index Z (x::xs) = x
6363index (S k) (x::xs) = index k xs
6464
65−||| Combine two streams element-wise using a function
66−zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c
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
70+zipWith : (f : a -> b -> c) -> (xs : Stream a) -> (ys : Stream b) -> Stream c
6771zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
6872
6973||| Combine three streams by applying a function element-wise along them