@@ -205,9 +205,18 @@ zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
205205zipWith f [] [] = []
206206zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
207207
208+||| Combine three equal-length vectors into a vector with some function
209+zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d
210+zipWith3 f [] [] [] = []
211+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
212+
208213||| Combine two equal-length vectors pairwise
209214zip : Vect n a -> Vect n b -> Vect n (a, b)
210−zip = zipWith (\x => \y => (x,y))
215+zip = zipWith (\x,y => (x,y))
216+
217+||| Combine three equal-length vectors elementwise into a vector of tuples
218+zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)
219+zip3 = zipWith3 (\x,y,z => (x,y,z))
211220
212221||| Convert a vector of pairs to a pair of vectors
213222unzip : Vect n (a, b) -> (Vect n a, Vect n b)
@@ -215,6 +224,12 @@ unzip [] = ([], [])
215224unzip ((l, r)::xs) with (unzip xs)
216225 | (lefts, rights) = (l::lefts, r::rights)
217226
227+||| Convert a vector of three-tuples to a triplet of vectors
228+unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)
229+unzip3 [] = ([], [], [])
230+unzip3 ((l,c,r)::xs) with (unzip3 xs)
231+ | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)
232+
218233--------------------------------------------------------------------------------
219234-- Equality
220235--------------------------------------------------------------------------------