@@ -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,9 +84,12 @@ 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
83−zip [] [] = []
84−zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)
92+zip = zipWith (\x => \y => (x,y))
8593
8694unzip : Vect (a, b) n -> (Vect a n, Vect b n)
8795unzip [] = ([], [])
@@ -122,6 +130,10 @@ foldr f e (x::xs) = f x (foldr f e xs)
122130-- Special folds
123131--------------------------------------------------------------------------------
124132
133+concat : Vect (Vect a n) m -> Vect a (m * n)
134+concat [] = []
135+concat (v::vs) = v ++ concat vs
136+
125137total and : Vect Bool m -> Bool
126138and = foldr (&&) True
127139