@@ -37,6 +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+||| Remove the element at the given position.
41+|||
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
47+
4048||| The intersectBy function returns the intersect of two lists by user-supplied equality predicate.
4149intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
4250intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]