@@ -12,11 +12,6 @@ using (xs : List a)
12 uninhabited Here impossible
12 uninhabited Here impossible
13 uninhabited (There p) impossible
13 uninhabited (There p) impossible
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
20 isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
15 isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
21 isElem x [] = No absurd
16 isElem x [] = No absurd
22 isElem x (y :: xs) with (decEq x y)
17 isElem x (y :: xs) with (decEq x y)
@@ -24,5 +19,12 @@ using (xs : List a)
24 isElem x (y :: xs) | (No contra) with (isElem x xs)
19 isElem x (y :: xs) | (No contra) with (isElem x xs)
25 isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
20 isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
26 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
21 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
23+ mkNo : {xs' : List a} ->
24+ ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
25+ Elem x' (y' :: xs') -> _|_
26+ mkNo f g Here = f refl
27+ mkNo f g (There x) = g x