@@ -37,6 +37,14 @@ isElem x (y :: xs) with (decEq x y)
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
40+||| Remove the element at the given position.
42+||| @xs The list to be removed from
43+||| @p A proof that the element to be removed is in the list
44+dropElem : (xs : List a) -> (p : Elem x xs) -> List a
45+dropElem (x :: ys) Here = ys
46+dropElem (x :: ys) (There p) = x :: dropElem ys p
40||| The intersectBy function returns the intersect of two lists by user-supplied equality predicate.
48||| The intersectBy function returns the intersect of two lists by user-supplied equality predicate.
41intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
49intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
42intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]
50intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]