@@ -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,9 +84,12 @@ 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
83−zip [] [] = []
92+zip = zipWith (\x => \y => (x,y))
84−zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)
86unzip : Vect (a, b) n -> (Vect a n, Vect b n)
94unzip : Vect (a, b) n -> (Vect a n, Vect b n)
87unzip [] = ([], [])
95unzip [] = ([], [])
@@ -122,6 +130,10 @@ foldr f e (x::xs) = f x (foldr f e xs)
122-- Special folds
130-- Special folds
123--------------------------------------------------------------------------------
131--------------------------------------------------------------------------------
133+concat : Vect (Vect a n) m -> Vect a (m * n)
135+concat (v::vs) = v ++ concat vs
125total and : Vect Bool m -> Bool
137total and : Vect Bool m -> Bool
126and = foldr (&&) True
138and = foldr (&&) True