@@ -19,6 +19,11 @@ implementation Uninhabited (Elem {a} x []) where
19 uninhabited Here impossible
19 uninhabited Here impossible
20 uninhabited (There p) impossible
20 uninhabited (There p) impossible
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
22||| Is the given element a member of the given list.
27||| Is the given element a member of the given list.
24||| @x The element to be tested.
29||| @x The element to be tested.
@@ -27,15 +32,9 @@ isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
27isElem x [] = No absurd
32isElem x [] = No absurd
28isElem x (y :: xs) with (decEq x y)
33isElem x (y :: xs) with (decEq x y)
29 isElem x (x :: xs) | (Yes Refl) = Yes Here
34 isElem x (x :: xs) | (Yes Refl) = Yes Here
30− isElem x (y :: xs) | (No contra) with (isElem x xs)
35+ isElem x (y :: xs) | (No xneqy) with (isElem x xs)
31− isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
36+ isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
32− isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
37+ isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
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
40||| Remove the element at the given position.
39||| Remove the element at the given position.