@@ -19,6 +19,11 @@ implementation Uninhabited (Elem {a} x []) where
1919 uninhabited Here impossible
2020 uninhabited (There p) impossible
2121
22+||| An item not in the head and not in the tail is not in the List at all
23+neitherHereNorThere : {x, y : a} -> {xs : List a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
24+neitherHereNorThere xneqy xninxs Here = xneqy Refl
25+neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs
26+
2227||| Is the given element a member of the given list.
2328|||
2429||| @x The element to be tested.
@@ -27,15 +32,9 @@ isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
2732isElem x [] = No absurd
2833isElem x (y :: xs) with (decEq x y)
2934 isElem x (x :: xs) | (Yes Refl) = Yes Here
30− isElem x (y :: xs) | (No contra) with (isElem x xs)
31− isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
32− isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
33− where
34− mkNo : {xs' : List a} ->
35− ((x' = y') -> Void) -> (Elem x' xs' -> Void) ->
36− Elem x' (y' :: xs') -> Void
37− mkNo f g Here = f Refl
38− mkNo f g (There x) = g x
35+ isElem x (y :: xs) | (No xneqy) with (isElem x xs)
36+ isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
37+ isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
3938
4039||| Remove the element at the given position.
4140|||