diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr index 4f09db46d..4bd9cb3ee 100644 --- a/libs/base/Data/List.idr +++ b/libs/base/Data/List.idr @@ -206,6 +206,31 @@ public export delete : Eq a => a -> List a -> List a delete = deleteBy (==) +||| Delete the first occurrence of each element from the second list in the first +||| list where equality is determined by the predicate passed as the first argument. +||| @ p A function that returns true when its two arguments should be considered equal. +||| @ source The list to delete elements from. +||| @ undesirables The list of elements to delete. +public export +deleteFirstsBy : (p : a -> a -> Bool) -> (source : List a) -> (undesirables : List a) -> List a +deleteFirstsBy p = foldl (flip (deleteBy p)) + +infix 7 \\ + +||| The non-associative list-difference. +||| A specialized form of @deleteFirstsBy@ where the predicate is equality under the @Eq@ +||| interface. +||| Deletes the first occurrence of each element of the second list from the first list. +||| +||| In the following example, the result is `[2, 4]`. +||| ```idris example +||| [1, 2, 3, 4] // [1, 3] +||| ``` +||| +public export +(\\) : (Eq a) => List a -> List a -> List a +(\\) = foldl (flip delete) + ||| The unionBy function returns the union of two lists by user-supplied equality predicate. public export unionBy : (a -> a -> Bool) -> List a -> List a -> List a