@@ -205,16 +205,31 @@ 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 xs ys zs
212+
208213||| Combine two equal-length vectors pairwise
209214zip : Vect n a -> Vect n b -> Vect n (a, b)
210215zip = zipWith (\x => \y => (x,y))
211216
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))
220+
212221||| Convert a vector of pairs to a pair of vectors
213222unzip : Vect n (a, b) -> (Vect n a, Vect n b)
214223unzip [] = ([], [])
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--------------------------------------------------------------------------------