@@ -593,12 +593,6 @@ isElem x (y :: xs) with (decEq x y)
593 isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
593 isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
594 isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
594 isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
596−||| A tactic for discovering where, if anywhere, an element is in a vector
597−||| @ n how many elements to search before giving up
598−findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic
599−findElem Z ctxt goal = Refine "Here" `Seq` Solve
600−findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
602replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
596replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
603replaceElem (x::xs) Here y = (y :: xs ** Here)
597replaceElem (x::xs) Here y = (y :: xs ** Here)
604replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
598replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)