@@ -1,11 +1,571 @@
11module Data.Vect
22
3+import public Data.Fin
34import Language.Reflection
4−import public Data.VectType
55
66%access public
77%default total
88
9+infixr 7 ::
10+
11+||| Vectors: Generic lists with explicit length in the type
12+%elim
13+data Vect : Nat -> Type -> Type where
14+ ||| Empty vector
15+ Nil : Vect Z a
16+ ||| A non-empty vector of length `S k`, consisting of a head element and
17+ ||| the rest of the list, of length `k`.
18+ (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
19+
20+-- Hints for interactive editing
21+%name Vect xs,ys,zs,ws
22+
23+--------------------------------------------------------------------------------
24+-- Length
25+--------------------------------------------------------------------------------
26+
27+||| Calculate the length of a `Vect`.
28+|||
29+||| **Note**: this is only useful if you don't already statically know the length
30+||| and you want to avoid matching the implicit argument for erasure reasons.
31+||| @ n the length (provably equal to the return value)
32+||| @ xs the vector
33+length : (xs : Vect n a) -> Nat
34+length [] = 0
35+length (x::xs) = 1 + length xs
36+
37+||| Show that the length function on vectors in fact calculates the length
38+private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
39+lengthCorrect Z [] = Refl
40+lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
41+
42+--------------------------------------------------------------------------------
43+-- Indexing into vectors
44+--------------------------------------------------------------------------------
45+
46+||| All but the first element of the vector
47+tail : Vect (S n) a -> Vect n a
48+tail (x::xs) = xs
49+
50+||| Only the first element of the vector
51+head : Vect (S n) a -> a
52+head (x::xs) = x
53+
54+||| The last element of the vector
55+last : Vect (S n) a -> a
56+last (x::[]) = x
57+last (x::y::ys) = last $ y::ys
58+
59+||| All but the last element of the vector
60+init : Vect (S n) a -> Vect n a
61+init (x::[]) = []
62+init (x::y::ys) = x :: init (y::ys)
63+
64+||| Extract a particular element from a vector
65+index : Fin n -> Vect n a -> a
66+index FZ (x::xs) = x
67+index (FS k) (x::xs) = index k xs
68+
69+
70+||| Insert an element at a particular index
71+insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
72+insertAt FZ y xs = y :: xs
73+insertAt (FS k) y (x::xs) = x :: insertAt k y xs
74+insertAt (FS k) y [] = absurd k
75+
76+||| Construct a new vector consisting of all but the indicated element
77+deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
78+deleteAt FZ (x::xs) = xs
79+deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs
80+deleteAt {n = Z} (FS k) (x::xs) = absurd k
81+deleteAt _ [] impossible
82+
83+||| Replace an element at a particlar index with another
84+replaceAt : Fin n -> t -> Vect n t -> Vect n t
85+replaceAt FZ y (x::xs) = y :: xs
86+replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
87+
88+||| Replace the element at a particular index with the result of applying a function to it
89+||| @ i the index to replace at
90+||| @ f the update function
91+||| @ xs the vector to replace in
92+updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t
93+updateAt FZ f (x::xs) = f x :: xs
94+updateAt (FS k) f (x::xs) = x :: updateAt k f xs
95+
96+--------------------------------------------------------------------------------
97+-- Subvectors
98+--------------------------------------------------------------------------------
99+
100+||| Get the first n elements of a Vect
101+||| @ n the number of elements to take
102+take : (n : Nat) -> Vect (n + m) a -> Vect n a
103+take Z xs = []
104+take (S k) (x :: xs) = x :: take k xs
105+
106+||| Remove the first n elements of a Vect
107+||| @ n the number of elements to remove
108+drop : (n : Nat) -> Vect (n + m) a -> Vect m a
109+drop Z xs = xs
110+drop (S k) (x :: xs) = drop k xs
111+
112+||| Take the longest prefix of a Vect such that all elements satisfy some
113+||| Boolean predicate.
114+|||
115+||| @ p the predicate
116+takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)
117+takeWhile p [] = (_ ** [])
118+takeWhile p (x::xs) =
119+ let (len ** ys) = takeWhile p xs
120+ in if p x then
121+ (S len ** x :: ys)
122+ else
123+ (_ ** [])
124+
125+||| Remove the longest prefix of a Vect such that all removed elements satisfy some
126+||| Boolean predicate.
127+|||
128+||| @ p the predicate
129+dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)
130+dropWhile p [] = (_ ** [])
131+dropWhile p (x::xs) =
132+ if p x then
133+ dropWhile p xs
134+ else
135+ (_ ** x::xs)
136+
137+--------------------------------------------------------------------------------
138+-- Transformations
139+--------------------------------------------------------------------------------
140+
141+||| Reverse the order of the elements of a vector
142+reverse : Vect n a -> Vect n a
143+reverse xs = go [] xs
144+ where go : Vect n a -> Vect m a -> Vect (n+m) a
145+ go {n} acc [] = rewrite plusZeroRightNeutral n in acc
146+ go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m
147+ in go (x::acc) xs
148+
149+||| Alternate an element between the other elements of a vector
150+||| @ sep the element to intersperse
151+||| @ xs the vector to separate with `sep`
152+intersperse : (sep : a) -> (xs : Vect n a) -> Vect (n + pred n) a
153+intersperse sep [] = []
154+intersperse sep (x::xs) = x :: intersperse' sep xs
155+ where
156+ intersperse' : a -> Vect n a -> Vect (n + n) a
157+ intersperse' sep [] = []
158+ intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n
159+ in sep :: x :: intersperse' sep xs
160+
161+--------------------------------------------------------------------------------
162+-- Conversion from list (toList is provided by Foldable)
163+--------------------------------------------------------------------------------
164+
165+
166+fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a
167+fromList' ys [] = ys
168+fromList' {n} ys (x::xs) =
169+ rewrite (plusSuccRightSucc (length xs) n) ==>
170+ Vect (plus (length xs) (S n)) a in
171+ fromList' (x::ys) xs
172+
173+||| Convert a list to a vector.
174+|||
175+||| The length of the list should be statically known.
176+fromList : (l : List a) -> Vect (length l) a
177+fromList l =
178+ rewrite (sym $ plusZeroRightNeutral (length l)) in
179+ reverse $ fromList' [] l
180+
181+--------------------------------------------------------------------------------
182+-- Building (bigger) vectors
183+--------------------------------------------------------------------------------
184+
185+||| Append two vectors
186+(++) : Vect m a -> Vect n a -> Vect (m + n) a
187+(++) [] ys = ys
188+(++) (x::xs) ys = x :: xs ++ ys
189+
190+||| Repeate some value n times
191+||| @ n the number of times to repeat it
192+||| @ x the value to repeat
193+replicate : (n : Nat) -> (x : a) -> Vect n a
194+replicate Z x = []
195+replicate (S k) x = x :: replicate k x
196+
197+--------------------------------------------------------------------------------
198+-- Zips and unzips
199+--------------------------------------------------------------------------------
200+
201+||| Combine two equal-length vectors pairwise with some function
202+zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
203+zipWith f [] [] = []
204+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
205+
206+||| Combine three equal-length vectors into a vector with some function
207+zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d
208+zipWith3 f [] [] [] = []
209+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
210+
211+||| Combine two equal-length vectors pairwise
212+zip : Vect n a -> Vect n b -> Vect n (a, b)
213+zip = zipWith (\x,y => (x,y))
214+
215+||| Combine three equal-length vectors elementwise into a vector of tuples
216+zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)
217+zip3 = zipWith3 (\x,y,z => (x,y,z))
218+
219+||| Convert a vector of pairs to a pair of vectors
220+unzip : Vect n (a, b) -> (Vect n a, Vect n b)
221+unzip [] = ([], [])
222+unzip ((l, r)::xs) with (unzip xs)
223+ | (lefts, rights) = (l::lefts, r::rights)
224+
225+||| Convert a vector of three-tuples to a triplet of vectors
226+unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)
227+unzip3 [] = ([], [], [])
228+unzip3 ((l,c,r)::xs) with (unzip3 xs)
229+ | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)
230+
231+--------------------------------------------------------------------------------
232+-- Equality
233+--------------------------------------------------------------------------------
234+
235+instance (Eq a) => Eq (Vect n a) where
236+ (==) [] [] = True
237+ (==) (x::xs) (y::ys) = x == y && xs == ys
238+
239+
240+--------------------------------------------------------------------------------
241+-- Order
242+--------------------------------------------------------------------------------
243+
244+instance Ord a => Ord (Vect n a) where
245+ compare [] [] = EQ
246+ compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys
247+
248+
249+--------------------------------------------------------------------------------
250+-- Maps
251+--------------------------------------------------------------------------------
252+
253+instance Functor (Vect n) where
254+ map f [] = []
255+ map f (x::xs) = f x :: map f xs
256+
257+
258+||| Map a partial function across a vector, returning those elements for which
259+||| the function had a value.
260+|||
261+||| The first projection of the resulting pair (ie the length) will always be
262+||| at most the length of the input vector. This is not, however, guaranteed
263+||| by the type.
264+|||
265+||| @ f the partial function (expressed by returning `Maybe`)
266+||| @ xs the vector to check for results
267+mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)
268+mapMaybe f [] = (_ ** [])
269+mapMaybe f (x::xs) =
270+ let (len ** ys) = mapMaybe f xs
271+ in case f x of
272+ Just y => (S len ** y :: ys)
273+ Nothing => ( len ** ys)
274+
275+
276+--------------------------------------------------------------------------------
277+-- Folds
278+--------------------------------------------------------------------------------
279+
280+foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
281+foldrImpl f e go [] = go e
282+foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
283+
284+instance Foldable (Vect n) where
285+ foldr f e xs = foldrImpl f e id xs
286+
287+--------------------------------------------------------------------------------
288+-- Special folds
289+--------------------------------------------------------------------------------
290+
291+||| Flatten a vector of equal-length vectors
292+concat : Vect m (Vect n a) -> Vect (m * n) a
293+concat [] = []
294+concat (v::vs) = v ++ concat vs
295+
296+||| Foldr without seeding the accumulator
297+foldr1 : (t -> t -> t) -> Vect (S n) t -> t
298+foldr1 f (x::xs) = foldr f x xs
299+
300+||| Foldl without seeding the accumulator
301+foldl1 : (t -> t -> t) -> Vect (S n) t -> t
302+foldl1 f (x::xs) = foldl f x xs
303+--------------------------------------------------------------------------------
304+-- Scans
305+--------------------------------------------------------------------------------
306+
307+scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b
308+scanl f q [] = [q]
309+scanl f q (x::xs) = q :: scanl f (f q x) xs
310+
311+--------------------------------------------------------------------------------
312+-- Membership tests
313+--------------------------------------------------------------------------------
314+
315+||| Search for an item using a user-provided test
316+||| @ p the equality test
317+||| @ e the item to search for
318+||| @ xs the vector to search in
319+elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool
320+elemBy p e [] = False
321+elemBy p e (x::xs) = p e x || elemBy p e xs
322+
323+||| Use the default Boolean equality on elements to search for an item
324+||| @ x what to search for
325+||| @ xs where to search
326+elem : Eq a => (x : a) -> (xs : Vect n a) -> Bool
327+elem = elemBy (==)
328+
329+||| Find the association of some key with a user-provided comparison
330+||| @ p the comparison operator for keys (True if they match)
331+||| @ e the key to look for
332+lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b
333+lookupBy p e [] = Nothing
334+lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
335+
336+||| Find the assocation of some key using the default Boolean equality test
337+lookup : Eq a => a -> Vect n (a, b) -> Maybe b
338+lookup = lookupBy (==)
339+
340+||| Check if any element of xs is found in elems by a user-provided comparison
341+||| @ p the comparison operator
342+||| @ elems the vector to search
343+||| @ xs what to search for
344+hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool
345+hasAnyBy p elems [] = False
346+hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
347+
348+||| Check if any element of xs is found in elems using the default Boolean equality test
349+hasAny : Eq a => Vect m a -> Vect n a -> Bool
350+hasAny = hasAnyBy (==)
351+
352+--------------------------------------------------------------------------------
353+-- Searching with a predicate
354+--------------------------------------------------------------------------------
355+
356+||| Find the first element of the vector that satisfies some test
357+||| @ p the test to satisfy
358+find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a
359+find p [] = Nothing
360+find p (x::xs) = if p x then Just x else find p xs
361+
362+||| Find the index of the first element of the vector that satisfies some test
363+findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
364+findIndex p [] = Nothing
365+findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
366+
367+||| Find the indices of all elements that satisfy some test
368+findIndices : (a -> Bool) -> Vect m a -> List (Fin m)
369+findIndices p [] = []
370+findIndices p (x :: xs) = let is = map FS $ findIndices p xs
371+ in if p x then 0 :: is else is
372+
373+elemIndexBy : (a -> a -> Bool) -> a -> Vect m a -> Maybe (Fin m)
374+elemIndexBy p e = findIndex $ p e
375+
376+elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
377+elemIndex = elemIndexBy (==)
378+
379+elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> List (Fin m)
380+elemIndicesBy p e = findIndices $ p e
381+
382+elemIndices : Eq a => a -> Vect m a -> List (Fin m)
383+elemIndices = elemIndicesBy (==)
384+
385+--------------------------------------------------------------------------------
386+-- Filters
387+--------------------------------------------------------------------------------
388+
389+||| Find all elements of a vector that satisfy some test
390+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
391+filter p [] = ( _ ** [] )
392+filter p (x::xs) =
393+ let (_ ** tail) = filter p xs
394+ in if p x then
395+ (_ ** x::tail)
396+ else
397+ (_ ** tail)
398+
399+||| Make the elements of some vector unique by some test
400+nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
401+nubBy = nubBy' []
402+ where
403+ nubBy' : Vect m a -> (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
404+ nubBy' acc p [] = (_ ** [])
405+ nubBy' acc p (x::xs) with (elemBy p x acc)
406+ | True = nubBy' acc p xs
407+ | False with (nubBy' (x::acc) p xs)
408+ | (_ ** tail) = (_ ** x::tail)
409+
410+||| Make the elements of some vector unique by the default Boolean equality
411+nub : Eq a => Vect n a -> (p ** Vect p a)
412+nub = nubBy (==)
413+
414+deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)
415+deleteBy _ _ [] = (_ ** [])
416+deleteBy eq x (y::ys) =
417+ let (len ** zs) = deleteBy eq x ys
418+ in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
419+
420+delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)
421+delete = deleteBy (==)
422+
423+--------------------------------------------------------------------------------
424+-- Splitting and breaking lists
425+--------------------------------------------------------------------------------
426+
427+||| A tuple where the first element is a Vect of the n first elements and
428+||| the second element is a Vect of the remaining elements of the original Vect
429+||| It is equivalent to (take n xs, drop n xs)
430+||| @ n the index to split at
431+||| @ xs the Vect to split in two
432+splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
433+splitAt n xs = (take n xs, drop n xs)
434+
435+partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))
436+partition p [] = ((_ ** []), (_ ** []))
437+partition p (x::xs) =
438+ let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in
439+ if p x then
440+ ((S leftLen ** x::lefts), (rightLen ** rights))
441+ else
442+ ((leftLen ** lefts), (S rightLen ** x::rights))
443+
444+--------------------------------------------------------------------------------
445+-- Predicates
446+--------------------------------------------------------------------------------
447+
448+isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
449+isPrefixOfBy p [] right = True
450+isPrefixOfBy p left [] = False
451+isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
452+
453+isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool
454+isPrefixOf = isPrefixOfBy (==)
455+
456+isSuffixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
457+isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
458+
459+isSuffixOf : Eq a => Vect m a -> Vect n a -> Bool
460+isSuffixOf = isSuffixOfBy (==)
461+
462+--------------------------------------------------------------------------------
463+-- Conversions
464+--------------------------------------------------------------------------------
465+
466+maybeToVect : Maybe a -> (p ** Vect p a)
467+maybeToVect Nothing = (_ ** [])
468+maybeToVect (Just j) = (_ ** [j])
469+
470+vectToMaybe : Vect n a -> Maybe a
471+vectToMaybe [] = Nothing
472+vectToMaybe (x::xs) = Just x
473+
474+--------------------------------------------------------------------------------
475+-- Misc
476+--------------------------------------------------------------------------------
477+
478+catMaybes : Vect n (Maybe a) -> (p ** Vect p a)
479+catMaybes [] = (_ ** [])
480+catMaybes (Nothing::xs) = catMaybes xs
481+catMaybes ((Just j)::xs) =
482+ let (_ ** tail) = catMaybes xs
483+ in (_ ** j::tail)
484+
485+diag : Vect n (Vect n a) -> Vect n a
486+diag [] = []
487+diag ((x::xs)::xss) = x :: diag (map tail xss)
488+
489+range : {n : Nat} -> Vect n (Fin n)
490+range {n=Z} = []
491+range {n=S _} = FZ :: map FS range
492+
493+||| Transpose a Vect of Vects, turning rows into columns and vice versa.
494+|||
495+||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
496+transpose : {n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a)
497+transpose [] = replicate _ []
498+transpose (x :: xs) = zipWith (::) x (transpose xs)
499+
500+--------------------------------------------------------------------------------
501+-- Applicative/Monad/Traversable
502+--------------------------------------------------------------------------------
503+
504+instance Applicative (Vect k) where
505+ pure = replicate _
506+
507+ fs <*> vs = zipWith apply fs vs
508+
509+||| This monad is different from the List monad, (>>=)
510+||| uses the diagonal.
511+instance Monad (Vect n) where
512+ m >>= f = diag (map f m)
513+
514+instance Traversable (Vect n) where
515+ traverse f [] = pure Vect.Nil
516+ traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
517+
518+--------------------------------------------------------------------------------
519+-- Show
520+--------------------------------------------------------------------------------
521+
522+instance Show a => Show (Vect n a) where
523+ show = show . toList
524+
525+--------------------------------------------------------------------------------
526+-- Properties
527+--------------------------------------------------------------------------------
528+
529+vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)
530+vectConsCong x xs xs Refl = Refl
531+
532+vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
533+vectNilRightNeutral [] = Refl
534+vectNilRightNeutral (x :: xs) =
535+ vectConsCong _ _ _ (vectNilRightNeutral xs)
536+
537+vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z
538+vectAppendAssociative [] y z = Refl
539+vectAppendAssociative (x :: xs) ys zs =
540+ vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
541+
542+--------------------------------------------------------------------------------
543+-- DecEq
544+--------------------------------------------------------------------------------
545+
546+vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
547+vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
548+
549+vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
550+vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
551+
552+instance DecEq a => DecEq (Vect n a) where
553+ decEq [] [] = Yes Refl
554+ decEq (x :: xs) (y :: ys) with (decEq x y)
555+ decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
556+ decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl
557+ decEq (x :: xs) (x :: ys) | Yes Refl | No neq = No (neq . vectInjective2)
558+ decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)
559+
560+{- The following definition is elaborated in a wrong case-tree. Examination pending.
561+instance DecEq a => DecEq (Vect n a) where
562+ decEq [] [] = Yes Refl
563+ decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)
564+ decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl
565+ decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
566+ decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
567+-}
568+
9569--------------------------------------------------------------------------------
10570-- Elem
11571--------------------------------------------------------------------------------
@@ -33,12 +593,6 @@ isElem x (y :: xs) with (decEq x y)
33593 isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
34594 isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)
35595
36−||| A tactic for discovering where, if anywhere, an element is in a vector
37−||| @ n how many elements to search before giving up
38−findElem : (n : Nat) -> List (TTName, Binder TT) -> TT -> Tactic
39−findElem Z ctxt goal = Refine "Here" `Seq` Solve
40−findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))
41−
42596replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)
43597replaceElem (x::xs) Here y = (y :: xs ** Here)
44598replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)