@@ -75,6 +75,19 @@ replicate : (n : Nat) -> a -> Vect a n
75replicate O x = []
75replicate O x = []
76replicate (S k) x = x :: replicate k x
76replicate (S k) x = x :: replicate k x
78+--------------------------------------------------------------------------------
80+--------------------------------------------------------------------------------
82+zip : Vect a n -> Vect b n -> Vect (a, b) n
84+zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)
86+unzip : Vect (a, b) n -> (Vect a n, Vect b n)
88+unzip ((l, r)::xs) with (unzip xs)
89+ | (lefts, rights) = (l::lefts, r::rights)
78--------------------------------------------------------------------------------
91--------------------------------------------------------------------------------
80--------------------------------------------------------------------------------
93--------------------------------------------------------------------------------