@@ -634,6 +634,14 @@ mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
634mapElem Here = Here
634mapElem Here = Here
635mapElem (There e) = There (mapElem e)
635mapElem (There e) = There (mapElem e)
637+||| Remove the element at the given position.
639+||| @xs The vector to be removed from
640+||| @p A proof that the element to be removed is in the vector
641+dropElem : (xs : Vect (S k) t) -> (p : Elem x xs) -> Vect k t
642+dropElem (x :: ys) Here = ys
643+dropElem {k = (S k)} (x :: ys) (There later) = x :: dropElem ys later
637-- Some convenience functions for testing lengths
645-- Some convenience functions for testing lengths
639||| If the given Vect is the required length, return a Vect with that
647||| If the given Vect is the required length, return a Vect with that