git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2173 from Heather/intersect
eea904dDavid Christiansen
libs/base/Data/List.idr+13
compare with master
unifiedsplit
@@ -36,3 +36,16 @@ isElem x (y :: xs) with (decEq x y)
36 Elem x' (y' :: xs') -> Void
36 Elem x' (y' :: xs') -> Void
37 mkNo f g Here = f Refl
37 mkNo f g Here = f Refl
38 mkNo f g (There x) = g x
38 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 (==)
536(\\) : (Eq a) => List a -> List a -> List a
536(\\) : (Eq a) => List a -> List a -> List a
537(\\) = foldl (flip delete)
537(\\) = foldl (flip delete)
538
538
539+||| The unionBy function returns the union of two lists by user-supplied equality predicate.
539unionBy : (a -> a -> Bool) -> List a -> List a -> List a
540unionBy : (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
541
542
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.
543|||
544|||
544||| ```idris example
545||| ```idris example
545||| union ['d', 'o', 'g'] ['c', 'o', 'w']
546||| union ['d', 'o', 'g'] ['c', 'o', 'w']