diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs index ecc2088..496be36 100644 --- a/src/Data/Vec.hs +++ b/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)