git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2173 from Heather/intersect

add intersect / intersectBy to Data.List

commiteea904d0d7f74e84904c9c8b7be98ebe20f7ab41 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 22 Apr 2015, 23:26 (12 years ago) parentb26c71c5f63dad
2 files changed+16−2
compare with master
unifiedsplit
libs/base/Data/List.idr+13 libs/prelude/Prelude/List.idr+3−2
libs/base/Data/List.idr+13
@@ -36,3 +36,16 @@ isElem x (y :: xs) with (decEq x y)
3636 Elem x' (y' :: xs') -> Void
3737 mkNo f g Here = f Refl
3838 mkNo f g (There x) = g x
39+
40+||| The intersectBy function returns the intersect of two lists by user-supplied equality predicate.
41+intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
42+intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
43+
44+||| Compute the intersection of two lists according to their `Eq` instance.
45+|||
46+||| ```idris example
47+||| intersect [1, 2, 3, 4] [2, 4, 6, 8]
48+||| ```
49+|||
50+intersect : (Eq a) => List a -> List a -> List a
51+intersect = intersectBy (==)
libs/prelude/Prelude/List.idr+3−2
@@ -536,10 +536,11 @@ delete = deleteBy (==)
536536(\\) : (Eq a) => List a -> List a -> List a
537537(\\) = foldl (flip delete)
538538
539+||| The unionBy function returns the union of two lists by user-supplied equality predicate.
539540unionBy : (a -> a -> Bool) -> List a -> List a -> List a
540−unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
541+unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
541542
542−||| The union function returns the list union of the two lists. For example,
543+||| Compute the union of two lists according to their `Eq` instance.
543544|||
544545||| ```idris example
545546||| union ['d', 'o', 'g'] ['c', 'o', 'w']