@@ -634,6 +634,14 @@ mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
634634mapElem Here = Here
635635mapElem (There e) = There (mapElem e)
636636
637+||| Remove the element at the given position.
638+|||
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
644+
637645-- Some convenience functions for testing lengths
638646
639647||| If the given Vect is the required length, return a Vect with that