@@ -75,6 +75,19 @@ replicate : (n : Nat) -> a -> Vect a n
7575replicate O x = []
7676replicate (S k) x = x :: replicate k x
7777
78+--------------------------------------------------------------------------------
79+-- Zips and unzips
80+--------------------------------------------------------------------------------
81+
82+zip : Vect a n -> Vect b n -> Vect (a, b) n
83+zip [] [] = []
84+zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)
85+
86+unzip : Vect (a, b) n -> (Vect a n, Vect b n)
87+unzip [] = ([], [])
88+unzip ((l, r)::xs) with (unzip xs)
89+ | (lefts, rights) = (l::lefts, r::rights)
90+
7891--------------------------------------------------------------------------------
7992-- Maps
8093--------------------------------------------------------------------------------