add "delete" functions

src/Data/Vec.hs

@@ -25,7 +25,6 @@ import Data.Maybe        (Maybe(..))
 import Data.Char         (Char)
 import Data.Function     ((∘), flip)
 import Data.Singletons   (SingI, sing)
-
 import Data.TypeClass
 
 
@@ -387,3 +386,20 @@ unzip ∷ Vec n (a, b) → (Vec n a, Vec n b)
 unzip Nil             = (Nil, Nil)
 unzip ((x, y) :- xys) = (x :- xs, y :- ys)
   where (xs, ys) = unzip xys
+
+
+-- * "Set" operations
+
+-- | 'delete' @x@ removes the first occurrence of @x@ from its list argument.
+-- For example,
+--
+-- > delete 'a' "banana" ≡ Just "bnana"
+delete ∷ Eq a ⇒ a → Vec (S n) a → Maybe (Vec n a)
+delete = deleteBy (≡)
+
+
+-- | The 'deleteBy' function behaves like 'delete', but takes a
+-- user-supplied equality predicate.
+deleteBy ∷ (a → a → 𝔹) → a → Vec (S n) a → Maybe (Vec n a)
+deleteBy (≃) t (x:-Nil)       = if t ≃ x then Just Nil else Nothing
+deleteBy (≃) t (x:-xs@(_:-_)) = if t ≃ x then Just xs  else fmap (x:-) (deleteBy (≃) t xs)