6310e0e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

add documentation to intersectBy and unionBY, change documentation for intersect, remove redundant patterns

commit6310e0e888fe2ee08b79510017006db076149e76 authorHeather <heather@live.ru> dateWed 22 Apr 2015, 14:02 (12 years ago) parent26b707a

2 files changed+5−7

unifiedsplit

libs/base/Data/List.idr+3−4

@@ -37,15 +37,14 @@ isElem x (y :: xs) with (decEq x y)

3737 mkNo f g Here = f Refl

3838 mkNo f g (There x) = g x

3939

40+||| The intersectBy function returns the intersect of two lists by user-supplied equality predicate.

4041intersectBy : (a -> a -> Bool) -> List a -> List a -> List a

41−intersectBy _ [] _ = []

42−intersectBy _ _ [] = []

4342intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]

4443

45−||| The intersect ∩ function returns the list intersect of the two lists. For example,

44+||| Compute the intersection of two lists according to their `Eq` instance.

4645|||

4746||| ```idris example

48−||| intersect [1,2,3,4] [2,4,6,8]

47+||| intersect [1, 2, 3, 4] [2, 4, 6, 8]

4948||| ```

5049|||

5150intersect : (Eq a) => List a -> List a -> List a

libs/prelude/Prelude/List.idr+2−3

@@ -536,12 +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 _ [] _ = []

541−unionBy _ _ [] = []

542541unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

543542

544−||| 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.

545544|||

546545||| ```idris example

547546||| union ['d', 'o', 'g'] ['c', 'o', 'w']