@@ -2,30 +2,29 @@ module Data.List
22
33%access public
44
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)
5+||| A proof that some element is found in a list
6+data Elem : a -> List a -> Type where
7+ Here : Elem x (x :: xs)
8+ There : Elem x xs -> Elem x (y :: xs)
109
11− instance Uninhabited (Elem {a} x []) where
12− uninhabited Here impossible
13− uninhabited (There p) impossible
10+instance Uninhabited (Elem {a} x []) where
11+ uninhabited Here impossible
12+ uninhabited (There p) impossible
1413
15− ||| Is the given element a member of the given list.
16− |||
17− ||| @x The element to be tested.
18− ||| @xs The list to be checked against
19− isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
20− isElem x [] = No absurd
21− isElem x (y :: xs) with (decEq x y)
22− isElem x (x :: xs) | (Yes refl) = Yes Here
23− isElem x (y :: xs) | (No contra) with (isElem x xs)
24− isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
25− isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
26− where
27− mkNo : {xs' : List a} ->
28− ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
29− Elem x' (y' :: xs') -> _|_
30− mkNo f g Here = f refl
31− mkNo f g (There x) = g x
14+||| Is the given element a member of the given list.
15+|||
16+||| @x The element to be tested.
17+||| @xs The list to be checked against
18+isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
19+isElem x [] = No absurd
20+isElem x (y :: xs) with (decEq x y)
21+ isElem x (x :: xs) | (Yes refl) = Yes Here
22+ isElem x (y :: xs) | (No contra) with (isElem x xs)
23+ isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
24+ isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
25+ where
26+ mkNo : {xs' : List a} ->
27+ ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
28+ Elem x' (y' :: xs') -> _|_
29+ mkNo f g Here = f refl
30+ mkNo f g (There x) = g x