git.iko.soy/Idris-dev
on master help sign in
add intersect to Data.List
26b707aHeather
libs/base/Data/List.idr+14
compare with master
unifiedsplit
@@ -36,3 +36,17 @@ 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+intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
41+intersectBy _ [] _ = []
42+intersectBy _ _ [] = []
43+intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
44+
45+||| The intersect ∩ function returns the list intersect of the two lists. For example,
46+|||
47+||| ```idris example
48+||| intersect [1,2,3,4] [2,4,6,8]
49+||| ```
50+|||
51+intersect : (Eq a) => List a -> List a -> List a
52+intersect = intersectBy (==)
libs/prelude/Prelude/List.idr+2
@@ -537,6 +537,8 @@ delete = deleteBy (==)
537(\\) = foldl (flip delete)
537(\\) = foldl (flip delete)
538
538
539unionBy : (a -> a -> Bool) -> List a -> List a -> List a
539unionBy : (a -> a -> Bool) -> List a -> List a -> List a
540+unionBy _ [] _ = []
541+unionBy _ _ [] = []
540unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
542unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs
541
543
542||| The union function returns the list union of the two lists. For example,
544||| The union function returns the list union of the two lists. For example,