@@ -0,0 +1,28 @@
1+module Data.List
2+
3+%access public
4+
5+using (xs : List a)
6+ ||| A proof that some element is found in a list
7+ data Elem : a -> List a -> Type where
8+ Here : Elem x (x :: xs)
9+ There : Elem x xs -> Elem x (y :: xs)
10+
11+ instance Uninhabited (Elem {a} x []) where
12+ uninhabited Here impossible
13+ uninhabited (There p) impossible
14+
15+ private
16+ mkNo : ((x = y) -> _|_) -> (Elem x xs -> _|_) -> Elem x (y :: xs) -> _|_
17+ mkNo f g Here = f refl
18+ mkNo f g (There x) = g x
19+
20+ isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
21+ isElem x [] = No absurd
22+ isElem x (y :: xs) with (decEq x y)
23+ isElem x (x :: xs) | (Yes refl) = Yes Here
24+ isElem x (y :: xs) | (No contra) with (isElem x xs)
25+ isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
26+ isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
27+
28+