@@ -36,6 +36,11 @@ index fO (x::xs) = x
36index (fS k) (x::xs) = index k xs
36index (fS k) (x::xs) = index k xs
37index fO [] impossible
37index fO [] impossible
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
39--------------------------------------------------------------------------------
44--------------------------------------------------------------------------------
40-- Subvectors
45-- Subvectors
41--------------------------------------------------------------------------------
46--------------------------------------------------------------------------------
@@ -79,6 +84,10 @@ replicate (S k) x = x :: replicate k x
79-- Zips and unzips
84-- Zips and unzips
80--------------------------------------------------------------------------------
85--------------------------------------------------------------------------------
87+zipWith : (a -> b -> c) -> Vect a n -> Vect b n -> Vect c n
89+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
82zip : Vect a n -> Vect b n -> Vect (a, b) n
91zip : Vect a n -> Vect b n -> Vect (a, b) n
83zip [] [] = []
92zip [] [] = []
84zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)
93zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)
@@ -122,6 +131,10 @@ foldr f e (x::xs) = f x (foldr f e xs)
122-- Special folds
131-- Special folds
123--------------------------------------------------------------------------------
132--------------------------------------------------------------------------------
134+concat : Vect (Vect a n) m -> Vect a (m * n)
136+concat (v::vs) = v ++ concat vs
125total and : Vect Bool m -> Bool
138total and : Vect Bool m -> Bool
126and = foldr (&&) True
139and = foldr (&&) True