@@ -36,6 +36,11 @@ index fO (x::xs) = x
3636index (fS k) (x::xs) = index k xs
3737index fO [] impossible
3838
39+deleteAt : Fin (S n) -> Vect a (S n) -> Vect a n
40+deleteAt fO (x::xs) = xs
41+deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
42+deleteAt _ [] impossible
43+
3944--------------------------------------------------------------------------------
4045-- Subvectors
4146--------------------------------------------------------------------------------
@@ -79,6 +84,10 @@ replicate (S k) x = x :: replicate k x
7984-- Zips and unzips
8085--------------------------------------------------------------------------------
8186
87+zipWith : (a -> b -> c) -> Vect a n -> Vect b n -> Vect c n
88+zipWith f [] [] = []
89+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
90+
8291zip : Vect a n -> Vect b n -> Vect (a, b) n
8392zip [] [] = []
8493zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)
@@ -122,6 +131,10 @@ foldr f e (x::xs) = f x (foldr f e xs)
122131-- Special folds
123132--------------------------------------------------------------------------------
124133
134+concat : Vect (Vect a n) m -> Vect a (m * n)
135+concat [] = []
136+concat (v::vs) = v ++ concat vs
137+
125138total and : Vect Bool m -> Bool
126139and = foldr (&&) True
127140