@@ -15,6 +15,24 @@ using (xs : Vect k a)
1515 Here : Elem x (x::xs)
1616 There : Elem x xs -> Elem x (y::xs)
1717
18+||| Nothing can be in an empty Vect
19+noEmptyElem : {x : a} -> Elem x [] -> _|_
20+noEmptyElem Here impossible
21+
22+||| An item not in the head and not in the tail is not in the Vect at all
23+neitherHereNorThere : {x, y : a} -> {xs : Vect n 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+
27+||| A decision procedure for Elem
28+isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
29+isElem x [] = No noEmptyElem
30+isElem x (y :: xs) with (decEq x y)
31+ isElem x (x :: xs) | (Yes refl) = Yes Here
32+ isElem x (y :: xs) | (No xneqy) with (isElem x xs)
33+ isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
34+ isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
35+
1836||| A tactic for discovering where, if anywhere, an element is in a vector
1937||| @ n how many elements to search before giving up
2038findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic