@@ -45,36 +45,64 @@ lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
45--------------------------------------------------------------------------------
45--------------------------------------------------------------------------------
47||| All but the first element of the vector
47||| All but the first element of the vector
48tail : Vect (S len) elem -> Vect len elem
52tail : Vect (S len) elem -> Vect len elem
49tail (x::xs) = xs
53tail (x::xs) = xs
51||| Only the first element of the vector
55||| Only the first element of the vector
52head : Vect (S len) elem -> elem
60head : Vect (S len) elem -> elem
53head (x::xs) = x
61head (x::xs) = x
55||| The last element of the vector
63||| The last element of the vector
56last : Vect (S len) elem -> elem
68last : Vect (S len) elem -> elem
57last (x::[]) = x
69last (x::[]) = x
58last (x::y::ys) = last $ y::ys
70last (x::y::ys) = last $ y::ys
60||| All but the last element of the vector
72||| All but the last element of the vector
61init : Vect (S len) elem -> Vect len elem
77init : Vect (S len) elem -> Vect len elem
62init (x::[]) = []
78init (x::[]) = []
63init (x::y::ys) = x :: init (y::ys)
79init (x::y::ys) = x :: init (y::ys)
65||| Extract a particular element from a vector
81||| Extract a particular element from a vector
66index : Fin len -> Vect len elem -> elem
86index : Fin len -> Vect len elem -> elem
67index FZ (x::xs) = x
87index FZ (x::xs) = x
68index (FS k) (x::xs) = index k xs
88index (FS k) (x::xs) = index k xs
71||| Insert an element at a particular index
91||| Insert an element at a particular index
94+||| insertAt 1 8 [1,2,3,4]
72insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
96insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
73insertAt FZ y xs = y :: xs
97insertAt FZ y xs = y :: xs
74insertAt (FS k) y (x::xs) = x :: insertAt k y xs
98insertAt (FS k) y (x::xs) = x :: insertAt k y xs
75insertAt (FS k) y [] = absurd k
99insertAt (FS k) y [] = absurd k
77||| Construct a new vector consisting of all but the indicated element
101||| Construct a new vector consisting of all but the indicated element
104+||| deleteAt 1 [1,2,3,4]
78deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
106deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
79deleteAt FZ (x::xs) = xs
107deleteAt FZ (x::xs) = xs
80deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
108deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
@@ -82,6 +110,10 @@ deleteAt {len = Z} (FS k) (x::xs) = absurd k
82deleteAt _ [] impossible
110deleteAt _ [] impossible
84||| Replace an element at a particlar index with another
112||| Replace an element at a particlar index with another
115+||| replaceAt 1 8 [1,2,3,4]
85replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
117replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
86replaceAt FZ y (x::xs) = y :: xs
118replaceAt FZ y (x::xs) = y :: xs
87replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
119replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
@@ -90,6 +122,10 @@ replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs
90||| @ i the index to replace at
122||| @ i the index to replace at
91||| @ f the update function
123||| @ f the update function
92||| @ xs the vector to replace in
124||| @ xs the vector to replace in
127+||| updateAt 1 (+10) [1,2,3,4]
93updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
129updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
94updateAt FZ f (x::xs) = f x :: xs
130updateAt FZ f (x::xs) = f x :: xs
95updateAt (FS k) f (x::xs) = x :: updateAt k f xs
131updateAt (FS k) f (x::xs) = x :: updateAt k f xs
@@ -100,44 +136,54 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
101||| Get the first n elements of a Vect
137||| Get the first n elements of a Vect
102||| @ n the number of elements to take
138||| @ n the number of elements to take
103take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
143take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
104take Z xs = []
144take Z xs = []
105take (S k) (x :: xs) = x :: take k xs
145take (S k) (x :: xs) = x :: take k xs
107−takeTake : (n : Nat) -> (m : Nat) -> (xs : Vect (n + m + l) a) -> take n (take (n + m) xs) = take n {m = m + l} (rewrite plusAssociative n m l in xs)
108−takeTake Z m xs = Refl
109−takeTake {l} (S k) m (x :: xs) = rewrite aux (plusAssociative k m l) x xs in cong { f = (x ::) } $ takeTake k m xs
110− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
111− (x : a) -> (xs : Vect m a) ->
112− rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
113− aux Refl x xs = Refl
115||| Remove the first n elements of a Vect
147||| Remove the first n elements of a Vect
116||| @ n the number of elements to remove
148||| @ n the number of elements to remove
117drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
153drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
118drop Z xs = xs
154drop Z xs = xs
119drop (S k) (x :: xs) = drop k xs
155drop (S k) (x :: xs) = drop k xs
121−dropDrop : (n : Nat) -> (m : Nat) -> (xs : Vect (m + n + l) a) -> drop n (drop m {m = n + l} (rewrite plusAssociative m n l in xs)) = drop (m + n) xs
157+||| Take up to the first n elements of a Vect if they exist.
122−dropDrop n Z xs = Refl
158+||| @ n the maximum number of elements to take
123−dropDrop {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in dropDrop n k xs
159+|||
124− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
160+||| ```idris example
125− (x : a) -> (xs : Vect m a) ->
161+||| takeUpto 10 [1,2,3,4]
126− rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
162+||| ```
127− aux Refl x xs = Refl
163+takeUpto : (x : Nat) -> Vect n elem -> Vect (minimum x n) elem
128−
164+takeUpto Z ys = []
129−takeDropDropTake : (n : Nat) -> (m : Nat) -> (xs : Vect (m + n + l) a) -> take n (drop m {m = n + l} (rewrite plusAssociative m n l in xs)) = drop m (take (m + n) xs)
165+takeUpto x [] = rewrite minimumZeroZeroLeft x in []
130−takeDropDropTake n Z xs = Refl
166+takeUpto (S x) (y::ys) = y :: takeUpto x ys
131−takeDropDropTake {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in takeDropDropTake n k xs
167+
132− where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
168+||| Drop up to the first n elements of a Vect if they exist.
133− (x : a) -> (xs : Vect m a) ->
169+||| @ n the maximum number of elements to remove.
134− rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
170+|||
135− aux Refl x xs = Refl
171+||| ```idris example
172+||| dropUpto 10 [1,2,3,4]
174+dropUpto : (x : Nat) -> Vect n elem -> Vect (n `minus` minimum x n) elem
175+dropUpto Z ys {n} = rewrite minusZeroRight n in ys
177+dropUpto (S x) (y :: ys) = dropUpto x ys
137||| Take the longest prefix of a Vect such that all elements satisfy some
179||| Take the longest prefix of a Vect such that all elements satisfy some
138||| Boolean predicate.
180||| Boolean predicate.
140||| @ p the predicate
182||| @ p the predicate
185+||| takeWhile (<3) [1,2,3,4]
141takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
187takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
142takeWhile p [] = (_ ** [])
188takeWhile p [] = (_ ** [])
143takeWhile p (x::xs) =
189takeWhile p (x::xs) =
@@ -151,6 +197,10 @@ takeWhile p (x::xs) =
151||| Boolean predicate.
197||| Boolean predicate.
153||| @ p the predicate
199||| @ p the predicate
202+||| dropWhile (<3) [1,2,3,4]
154dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
204dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
155dropWhile p [] = (_ ** [])
205dropWhile p [] = (_ ** [])
156dropWhile p (x::xs) =
206dropWhile p (x::xs) =
@@ -164,6 +214,10 @@ dropWhile p (x::xs) =
164--------------------------------------------------------------------------------
214--------------------------------------------------------------------------------
166||| Reverse the order of the elements of a vector
216||| Reverse the order of the elements of a vector
219+||| reverse [1,2,3,4]
167reverse : Vect len elem -> Vect len elem
221reverse : Vect len elem -> Vect len elem
168reverse xs = go [] xs
222reverse xs = go [] xs
169 where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
223 where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
@@ -174,6 +228,10 @@ reverse xs = go [] xs
174||| Alternate an element between the other elements of a vector
228||| Alternate an element between the other elements of a vector
175||| @ sep the element to intersperse
229||| @ sep the element to intersperse
176||| @ xs the vector to separate with `sep`
230||| @ xs the vector to separate with `sep`
233+||| intersperse 0 [1,2,3,4]
177intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
235intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
178intersperse sep [] = []
236intersperse sep [] = []
179intersperse sep (x::xs) = x :: intersperse' sep xs
237intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -198,6 +256,10 @@ fromList' {len} ys (x::xs) =
198||| Convert a list to a vector.
256||| Convert a list to a vector.
200||| The length of the list should be statically known.
258||| The length of the list should be statically known.
261+||| fromList [1,2,3,4]
201fromList : (l : List elem) -> Vect (length l) elem
263fromList : (l : List elem) -> Vect (length l) elem
202fromList l =
264fromList l =
203 rewrite (sym $ plusZeroRightNeutral (length l)) in
265 rewrite (sym $ plusZeroRightNeutral (length l)) in
@@ -208,31 +270,31 @@ fromList l =
208--------------------------------------------------------------------------------
270--------------------------------------------------------------------------------
210||| Append two vectors
272||| Append two vectors
275+||| [1,2,3,4] ++ [5,6]
211(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
277(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
212(++) [] ys = ys
278(++) [] ys = ys
213(++) (x::xs) ys = x :: xs ++ ys
279(++) (x::xs) ys = x :: xs ++ ys
215−takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
216−takePrefix [] _ = Refl
217−takePrefix (n :: ns) ms = cong $ takePrefix ns ms
219−dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
220−dropPrefix [] ms = Refl
221−dropPrefix (_ :: ns) ms = dropPrefix ns ms
223−takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
224−takeDropConcat Z xs = Refl
225−takeDropConcat (S k) (x :: xs) = cong $ takeDropConcat k xs
227−||| Repeate some value some number of times.
281+||| Repeat some value some number of times.
229||| @ len the number of times to repeat it
283||| @ len the number of times to repeat it
230||| @ x the value to repeat
284||| @ x the value to repeat
231replicate : (len : Nat) -> (x : elem) -> Vect len elem
289replicate : (len : Nat) -> (x : elem) -> Vect len elem
232replicate Z x = []
290replicate Z x = []
233replicate (S k) x = x :: replicate k x
291replicate (S k) x = x :: replicate k x
235||| Merge two ordered vectors
293||| Merge two ordered vectors
296+||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
236mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
298mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
237mergeBy order [] [] = []
299mergeBy order [] [] = []
238mergeBy order [] (x :: xs) = x :: xs
300mergeBy order [] (x :: xs) = x :: xs
@@ -256,30 +318,54 @@ merge = mergeBy compare
256||| @ f the function to combine elements with
318||| @ f the function to combine elements with
257||| @ xs the first vector of elements
319||| @ xs the first vector of elements
258||| @ ys the second vector of elements
320||| @ ys the second vector of elements
323+||| zipWith (+) (fromList [1,2,3,4]) (fromList [5,6,7,8])
259zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
325zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
260zipWith f [] [] = []
326zipWith f [] [] = []
261zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
327zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
263||| Combine three equal-length vectors into a vector with some function
329||| Combine three equal-length vectors into a vector with some function
332+||| zipWith3 (\x,y,z => x+y+z) (fromList [1,2,3,4]) (fromList [5,6,7,8]) (fromList [1,1,1,1])
264zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
334zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
265zipWith3 f [] [] [] = []
335zipWith3 f [] [] [] = []
266zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
336zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
268||| Combine two equal-length vectors pairwise
338||| Combine two equal-length vectors pairwise
341+||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])
269zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
343zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
270zip = zipWith (\x,y => (x,y))
344zip = zipWith (\x,y => (x,y))
272||| Combine three equal-length vectors elementwise into a vector of tuples
346||| Combine three equal-length vectors elementwise into a vector of tuples
349+||| zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])
273zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
351zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
274zip3 = zipWith3 (\x,y,z => (x,y,z))
352zip3 = zipWith3 (\x,y,z => (x,y,z))
276||| Convert a vector of pairs to a pair of vectors
354||| Convert a vector of pairs to a pair of vectors
357+||| unzip (fromList [(1,2), (1,2)])
277unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
359unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
278unzip [] = ([], [])
360unzip [] = ([], [])
279unzip ((l, r)::xs) with (unzip xs)
361unzip ((l, r)::xs) with (unzip xs)
280 | (lefts, rights) = (l::lefts, r::rights)
362 | (lefts, rights) = (l::lefts, r::rights)
282||| Convert a vector of three-tuples to a triplet of vectors
364||| Convert a vector of three-tuples to a triplet of vectors
367+||| unzip3 (fromList [(1,2,3), (1,2,3)])
283unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
369unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
284unzip3 [] = ([], [], [])
370unzip3 [] = ([], [], [])
285unzip3 ((l,c,r)::xs) with (unzip3 xs)
371unzip3 ((l,c,r)::xs) with (unzip3 xs)
@@ -321,6 +407,10 @@ implementation Functor (Vect n) where
322||| @ f the partial function (expressed by returning `Maybe`)
408||| @ f the partial function (expressed by returning `Maybe`)
323||| @ xs the vector to check for results
409||| @ xs the vector to check for results
412+||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
324mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
414mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
325mapMaybe f [] = (_ ** [])
415mapMaybe f [] = (_ ** [])
326mapMaybe f (x::xs) =
416mapMaybe f (x::xs) =
@@ -329,7 +419,6 @@ mapMaybe f (x::xs) =
329 Just y => (S len ** y :: ys)
419 Just y => (S len ** y :: ys)
330 Nothing => ( len ** ys)
420 Nothing => ( len ** ys)
333--------------------------------------------------------------------------------
422--------------------------------------------------------------------------------
335--------------------------------------------------------------------------------
424--------------------------------------------------------------------------------
@@ -346,15 +435,28 @@ implementation Foldable (Vect n) where
346--------------------------------------------------------------------------------
435--------------------------------------------------------------------------------
348||| Flatten a vector of equal-length vectors
437||| Flatten a vector of equal-length vectors
440+||| concat [[1,2,3], [4,5,6]]
349concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
442concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
350concat [] = []
443concat [] = []
351concat (v::vs) = v ++ concat vs
444concat (v::vs) = v ++ concat vs
353||| Foldr without seeding the accumulator
446||| Foldr without seeding the accumulator
449+||| foldr1 (-) (fromList [1,2,3])
354foldr1 : (t -> t -> t) -> Vect (S n) t -> t
451foldr1 : (t -> t -> t) -> Vect (S n) t -> t
355−foldr1 f (x::xs) = foldr f x xs
452+foldr1 f [x] = x
453+foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
357||| Foldl without seeding the accumulator
455||| Foldl without seeding the accumulator
458+||| foldl1 (-) (fromList [1,2,3])
358foldl1 : (t -> t -> t) -> Vect (S n) t -> t
460foldl1 : (t -> t -> t) -> Vect (S n) t -> t
359foldl1 f (x::xs) = foldl f x xs
461foldl1 f (x::xs) = foldl f x xs
@@ -364,6 +466,10 @@ foldl1 f (x::xs) = foldl f x xs
365||| The scanl function is similar to foldl, but returns all the intermediate
467||| The scanl function is similar to foldl, but returns all the intermediate
366||| accumulator states in the form of a vector.
468||| accumulator states in the form of a vector.
471+||| scanl (-) 0 (fromList [1,2,3])
367scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
473scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
368scanl f q [] = [q]
474scanl f q [] = [q]
369scanl f q (x::xs) = q :: scanl f (f q x) xs
475scanl f q (x::xs) = q :: scanl f (f q x) xs
@@ -372,6 +478,10 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
372||| starting value.
478||| starting value.
373||| It assumes the first element of the vector to be the starting value and then
479||| It assumes the first element of the vector to be the starting value and then
374||| starts the fold with the element following it.
480||| starts the fold with the element following it.
483+||| scanl1 (-) (fromList [1,2,3])
375scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
485scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
376scanl1 f [] = []
486scanl1 f [] = []
377scanl1 f (x::xs) = scanl f x xs
487scanl1 f (x::xs) = scanl f x xs
@@ -384,6 +494,10 @@ scanl1 f (x::xs) = scanl f x xs
384||| @ p the equality test
494||| @ p the equality test
385||| @ e the item to search for
495||| @ e the item to search for
386||| @ xs the vector to search in
496||| @ xs the vector to search in
499+||| elemBy (==) 2 [1,2,3,4]
387elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
501elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
388elemBy p e [] = False
502elemBy p e [] = False
389elemBy p e (x::xs) = p e x || elemBy p e xs
503elemBy p e (x::xs) = p e x || elemBy p e xs
@@ -391,17 +505,29 @@ elemBy p e (x::xs) = p e x || elemBy p e xs
391||| Use the default Boolean equality on elements to search for an item
505||| Use the default Boolean equality on elements to search for an item
392||| @ x what to search for
506||| @ x what to search for
393||| @ xs where to search
507||| @ xs where to search
394elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
512elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
395elem = elemBy (==)
513elem = elemBy (==)
397||| Find the association of some key with a user-provided comparison
515||| Find the association of some key with a user-provided comparison
398||| @ p the comparison operator for keys (True if they match)
516||| @ p the comparison operator for keys (True if they match)
399||| @ e the key to look for
517||| @ e the key to look for
520+||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
400lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
522lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
401lookupBy p e [] = Nothing
523lookupBy p e [] = Nothing
402lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
524lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
404||| Find the assocation of some key using the default Boolean equality test
526||| Find the assocation of some key using the default Boolean equality test
529+||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
405lookup : Eq key => key -> Vect n (key, val) -> Maybe val
531lookup : Eq key => key -> Vect n (key, val) -> Maybe val
406lookup = lookupBy (==)
532lookup = lookupBy (==)
@@ -409,11 +535,19 @@ lookup = lookupBy (==)
409||| @ p the comparison operator
535||| @ p the comparison operator
410||| @ elems the vector to search
536||| @ elems the vector to search
411||| @ xs what to search for
537||| @ xs what to search for
540+||| hasAnyBy (==) [2,5] [1,2,3,4]
412hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
542hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
413hasAnyBy p elems [] = False
543hasAnyBy p elems [] = False
414hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
544hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
416||| Check if any element of xs is found in elems using the default Boolean equality test
546||| Check if any element of xs is found in elems using the default Boolean equality test
549+||| hasAny [2,5] [1,2,3,4]
417hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
551hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
418hasAny = hasAnyBy (==)
552hasAny = hasAnyBy (==)
@@ -423,30 +557,62 @@ hasAny = hasAnyBy (==)
424||| Find the first element of the vector that satisfies some test
558||| Find the first element of the vector that satisfies some test
425||| @ p the test to satisfy
559||| @ p the test to satisfy
562+||| find (== 3) [1,2,3,4]
426find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
564find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
427find p [] = Nothing
565find p [] = Nothing
428find p (x::xs) = if p x then Just x else find p xs
566find p (x::xs) = if p x then Just x else find p xs
430||| Find the index of the first element of the vector that satisfies some test
568||| Find the index of the first element of the vector that satisfies some test
571+||| findIndex (== 3) [1,2,3,4]
431findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
573findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
432findIndex p [] = Nothing
574findIndex p [] = Nothing
433findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
575findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
435||| Find the indices of all elements that satisfy some test
577||| Find the indices of all elements that satisfy some test
580+||| findIndices (< 3) [1,2,3,4]
436findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
582findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
437findIndices p [] = []
583findIndices p [] = []
438findIndices p (x :: xs) = let is = map FS $ findIndices p xs
584findIndices p (x :: xs) = let is = map FS $ findIndices p xs
439 in if p x then 0 :: is else is
585 in if p x then 0 :: is else is
587+||| Find the index of the first element of the vector that satisfies some test
590+||| elemIndexBy (==) 3 [1,2,3,4]
441elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
592elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
442elemIndexBy p e = findIndex $ p e
593elemIndexBy p e = findIndex $ p e
595+||| Find the index of the first element of the vector equal to the given one.
598+||| elemIndex 3 [1,2,3,4]
444elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
600elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
445elemIndex = elemIndexBy (==)
601elemIndex = elemIndexBy (==)
603+||| Find the indices of all elements that satisfy some test
606+||| elemIndicesBy (<=) 3 [1,2,3,4]
447elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
608elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
448elemIndicesBy p e = findIndices $ p e
609elemIndicesBy p e = findIndices $ p e
611+||| Find the indices of all elements uquals to the given one
614+||| elemIndices 3 [1,2,3,4,3]
450elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
616elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
451elemIndices = elemIndicesBy (==)
617elemIndices = elemIndicesBy (==)
@@ -455,6 +621,10 @@ elemIndices = elemIndicesBy (==)
455--------------------------------------------------------------------------------
621--------------------------------------------------------------------------------
457||| Find all elements of a vector that satisfy some test
623||| Find all elements of a vector that satisfy some test
626+||| filter (< 3) (fromList [1,2,3,4])
458filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
628filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
459filter p [] = ( _ ** [] )
629filter p [] = ( _ ** [] )
460filter p (x::xs) =
630filter p (x::xs) =
@@ -465,6 +635,10 @@ filter p (x::xs) =
465 (_ ** tail)
635 (_ ** tail)
467||| Make the elements of some vector unique by some test
637||| Make the elements of some vector unique by some test
640+||| nubBy (==) (fromList [1,2,2,3,4,4])
468nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
642nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
469nubBy = nubBy' []
643nubBy = nubBy' []
@@ -476,15 +650,29 @@ nubBy = nubBy' []
476 | (_ ** tail) = (_ ** x::tail)
650 | (_ ** tail) = (_ ** x::tail)
478||| Make the elements of some vector unique by the default Boolean equality
652||| Make the elements of some vector unique by the default Boolean equality
655+||| nub (fromList [1,2,2,3,4,4])
479nub : Eq elem => Vect len elem -> (p ** Vect p elem)
657nub : Eq elem => Vect len elem -> (p ** Vect p elem)
480nub = nubBy (==)
658nub = nubBy (==)
660+||| Delete first element from list according to some test
663+||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
482deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
665deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
483deleteBy _ _ [] = (_ ** [])
666deleteBy _ _ [] = (_ ** [])
484deleteBy eq x (y::ys) =
667deleteBy eq x (y::ys) =
485 let (len ** zs) = deleteBy eq x ys
668 let (len ** zs) = deleteBy eq x ys
486 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
669 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
671+||| Delete first element from list equal to the given one
674+||| delete 2 (fromList [1,2,2,3,4,4])
488delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
676delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
489delete = deleteBy (==)
677delete = deleteBy (==)
@@ -494,25 +682,26 @@ delete = deleteBy (==)
495||| A tuple where the first element is a `Vect` of the `n` first elements and
683||| A tuple where the first element is a `Vect` of the `n` first elements and
496||| the second element is a `Vect` of the remaining elements of the original.
684||| the second element is a `Vect` of the remaining elements of the original.
497−||| It is equivalent to `(take n xs, drop n xs)`, but is more efficient.
685+||| It is equivalent to `(take n xs, drop n xs)` (`splitAtTakeDrop`),
686+||| but is more efficient.
498||| @ n the index to split at
688||| @ n the index to split at
499−||| @ xs the Vect to split in two
689+||| @ xs the `Vect` to split in two
692+||| splitAt 2 (fromList [1,2,3,4])
500splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
694splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
501splitAt Z xs = ([], xs)
695splitAt Z xs = ([], xs)
502−splitAt (S k) (x::xs) =
696+splitAt (S k) (x :: xs) with (splitAt k xs)
503− let (tk, dr) = splitAt k xs
506−splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
507−splitAtTakeDrop Z xs = Refl
508−splitAtTakeDrop (S k) (x::xs) with (splitAt k xs) proof p
509− | (tk, dr) =
697+ | (tk, dr) = (x :: tk, dr)
510− let rec = sym $ trans p $ splitAtTakeDrop k xs
511− tkp = cong {f=fst} rec
512− drp = cong {f=snd} rec
513− in replace {P = \tk' => (x::tk', dr) = (x::take k xs, drop k xs)} tkp $
514− replace {P = \dr' => (x::take k xs, dr') = (x::take k xs, drop k xs) } drp Refl
699+||| A tuple where the first element is a `Vect` of the `n` elements passing given test
700+||| and the second element is a `Vect` of the remaining elements of the original.
703+||| partition (== 2) (fromList [1,2,3,2,4])
516partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
705partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
517partition p [] = ((_ ** []), (_ ** []))
706partition p [] = ((_ ** []), (_ ** []))
518partition p (x::xs) =
707partition p (x::xs) =
@@ -526,17 +715,37 @@ partition p (x::xs) =
526-- Predicates
715-- Predicates
527--------------------------------------------------------------------------------
716--------------------------------------------------------------------------------
718+||| Verify vector prefix
721+||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
529isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
723isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
530isPrefixOfBy p [] right = True
724isPrefixOfBy p [] right = True
531isPrefixOfBy p left [] = False
725isPrefixOfBy p left [] = False
532isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
726isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
728+||| Verify vector prefix
731+||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
534isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
733isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
535isPrefixOf = isPrefixOfBy (==)
734isPrefixOf = isPrefixOfBy (==)
736+||| Verify vector suffix
739+||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
537isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
741isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
538isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
742isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
744+||| Verify vector suffix
747+||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
540isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
749isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
541isSuffixOf = isSuffixOfBy (==)
750isSuffixOf = isSuffixOfBy (==)
@@ -544,10 +753,20 @@ isSuffixOf = isSuffixOfBy (==)
544-- Conversions
753-- Conversions
545--------------------------------------------------------------------------------
754--------------------------------------------------------------------------------
756+||| Convert Maybe type into Vect
759+||| maybeToVect (Just 2)
547maybeToVect : Maybe elem -> (p ** Vect p elem)
761maybeToVect : Maybe elem -> (p ** Vect p elem)
548maybeToVect Nothing = (_ ** [])
762maybeToVect Nothing = (_ ** [])
549maybeToVect (Just j) = (_ ** [j])
763maybeToVect (Just j) = (_ ** [j])
765+||| Convert first element of Vect (if exists) into Maybe.
551vectToMaybe : Vect len elem -> Maybe elem
770vectToMaybe : Vect len elem -> Maybe elem
552vectToMaybe [] = Nothing
771vectToMaybe [] = Nothing
553vectToMaybe (x::xs) = Just x
772vectToMaybe (x::xs) = Just x
@@ -556,6 +775,11 @@ vectToMaybe (x::xs) = Just x
557--------------------------------------------------------------------------------
776--------------------------------------------------------------------------------
778+||| Filter out Nothings from Vect
781+||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
559catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
783catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
560catMaybes [] = (_ ** [])
784catMaybes [] = (_ ** [])
561catMaybes (Nothing::xs) = catMaybes xs
785catMaybes (Nothing::xs) = catMaybes xs
@@ -563,6 +787,11 @@ catMaybes ((Just j)::xs) =
563 let (_ ** tail) = catMaybes xs
787 let (_ ** tail) = catMaybes xs
564 in (_ ** j::tail)
788 in (_ ** j::tail)
790+||| Get diagonal elements
793+||| diag [[1,2,3], [4,5,6], [7,8,9]]
566diag : Vect len (Vect len elem) -> Vect len elem
795diag : Vect len (Vect len elem) -> Vect len elem
567diag [] = []
796diag [] = []
568diag ((x::xs)::xss) = x :: diag (map tail xss)
797diag ((x::xs)::xss) = x :: diag (map tail xss)
@@ -573,9 +802,13 @@ range {len=S _} = FZ :: map FS range
574||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
803||| Transpose a `Vect` of `Vect`s, turning rows into columns and vice versa.
576−||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id`.
805+||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
578||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
807||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
810+||| transpose [[1,2], [3,4], [5,6], [7,8]]
579transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
812transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
580transpose [] = replicate _ [] -- = [| [] |]
813transpose [] = replicate _ [] -- = [| [] |]
581transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
814transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]
@@ -594,8 +827,8 @@ implementation Monad (Vect len) where
594 m >>= f = diag (map f m)
827 m >>= f = diag (map f m)
596implementation Traversable (Vect n) where
829implementation Traversable (Vect n) where
597− traverse f [] = pure []
830+ traverse f [] = [| [] |]
598− traverse f (x::xs) = [| f x :: traverse f xs |]
831+ traverse f (x :: xs) = [| f x :: traverse f xs |]
600--------------------------------------------------------------------------------
833--------------------------------------------------------------------------------
@@ -615,11 +848,17 @@ Uninhabited a => Uninhabited (Vect (S n) a) where
615-- Properties
848-- Properties
616--------------------------------------------------------------------------------
849--------------------------------------------------------------------------------
851+vectMustBeNil : (xs : Vect Z a) -> xs = []
852+vectMustBeNil [] = Refl
618vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
854vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
619vectConsCong x xs xs Refl = Refl
855vectConsCong x xs xs Refl = Refl
621−vectMustBeNil : (xs : Vect Z a) -> xs = []
857+vectInjective1 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> x ~=~ y
622−vectMustBeNil [] = Refl
858+vectInjective1 Refl = Refl
860+vectInjective2 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> xs ~=~ ys
861+vectInjective2 Refl = Refl
624vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
863vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
625vectNilRightNeutral [] = Refl
864vectNilRightNeutral [] = Refl
@@ -634,16 +873,93 @@ vectAppendAssociative [] y z = Refl
634vectAppendAssociative (x :: xs) ys zs =
873vectAppendAssociative (x :: xs) ys zs =
635 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
874 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
876+||| Adding a prefix and then taking the prefix gets the prefix. Or,
877+||| adding a suffix and then dropping the suffix does nothing.
878+takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
879+takePrefix [] _ = Refl
880+takePrefix (n :: ns) ms = cong $ takePrefix ns ms
882+||| Adding a prefix and then dropping the prefix does nothing. Or,
883+||| adding a suffix and then taking the suffix gets the suffix.
884+dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
885+dropPrefix [] ms = Refl
886+dropPrefix (_ :: ns) ms = dropPrefix ns ms
888+||| `take n . take (n + m) = take n`
889+takeTake : (n : Nat) -> (m : Nat) ->
890+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
892+ take n (take (n + m) xs) = take n ys
893+takeTake Z m _ _ _ = Refl
894+takeTake (S n) m (x :: xs) (y :: ys) prf = rewrite vectInjective1 prf in cong (takeTake n m xs ys (vectInjective2 prf))
896+||| `drop (n + m) = drop m . drop n`
897+dropDrop : (n : Nat) -> (m : Nat) ->
898+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
900+ drop (n + m) xs = drop m (drop n ys)
901+dropDrop Z m xs xs Refl = Refl
902+dropDrop (S n) m (_ :: xs) (_ :: ys) prf = dropDrop n m xs ys (vectInjective2 prf)
904+||| A `Vect` may be restored from its components.
905+takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
906+takeDropConcat Z xs = Refl
907+takeDropConcat (S n) (x :: xs) = cong $ takeDropConcat n xs
909+||| `drop n . take (n + m) = take m . drop n`.
911+||| Or: there are two ways to extract a subsequence.
912+dropTakeTakeDrop : (n : Nat) -> (m : Nat) ->
913+ (xs : Vect ((n + m) + l) a) -> (ys : Vect (n + (m + l)) a) ->
915+ drop n (take (n + m) xs) = take m (drop n ys)
916+dropTakeTakeDrop Z m xs xs Refl = Refl
917+dropTakeTakeDrop (S n) m (_ :: xs) (_ :: ys) prf = dropTakeTakeDrop n m xs ys (vectInjective2 prf)
919+splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
920+splitAtTakeDrop Z xs = Refl
921+splitAtTakeDrop (S k) (x :: xs) with (splitAt k xs) proof p
922+ | (tk, dr) = let prf = trans p (splitAtTakeDrop k xs)
923+ in aux (cong {f=(x ::) . fst} prf) (cong {f=snd} prf)
924+ where aux : {a, b : Type} -> {w, x : a} -> {y, z : b} -> w = x -> y = z -> (w, y) = (x, z)
925+ aux Refl Refl = Refl
927+zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = [| f as bs |]
928+zipWithIsLiftA2 _ [] [] = Refl
929+zipWithIsLiftA2 f (a :: as) (b :: bs) = rewrite zipWithIsLiftA2 f as bs in Refl
930+zipWithIsLiftA3 : (f : a -> b -> c -> d) -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> zipWith3 f as bs cs = [| f as bs cs |]
931+zipWithIsLiftA3 _ [] [] [] = Refl
932+zipWithIsLiftA3 f (a :: as) (b :: bs) (c :: cs) = rewrite zipWithIsLiftA3 f as bs cs in Refl
934+-- Note relationship to Applicative (Morphism (Fin n))
935+indexReplicate : (x : a) -> (n : Nat) -> (i : Fin n) -> index i (replicate n x) = x
936+indexReplicate x (S n) FZ = Refl
937+indexReplicate x (S n) (FS i) = indexReplicate x n i
938+indexZipWith : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> (i : Fin n) -> index i (zipWith f as bs) = f (index i as) (index i bs)
939+indexZipWith f (a :: _) (b :: _) FZ = Refl
940+indexZipWith f (_ :: as) (_ :: bs) (FS i) = indexZipWith f as bs i
941+indexTranspose : (x : Fin o) -> (y : Fin i) -> (xss : Vect o (Vect i a)) -> index y (index x xss) = index x (index y (transpose xss))
942+indexTranspose x y (xs :: xss) = rewrite prf in
943+ rewrite sym $ indexZipWith Vect.(::) xs (transpose xss) y in Refl
944+ where prf : index y (index x (xs :: xss)) = index x (index y xs :: index y (transpose xss))
947+ FS k => indexTranspose k y xss
949+transposeTraverse : (xss : Vect o (Vect i a)) -> transpose xss = traverse Basics.id xss
950+transposeTraverse [] = Refl
951+transposeTraverse (xs :: xss) = rewrite zipWithIsLiftA2 Vect.(::) xs (transpose xss) in cong (transposeTraverse xss)
953+traverseIdCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> traverse Basics.id [| xs :: xss |] = xs :: traverse Basics.id xss
954+traverseIdCons [] [] = Refl
955+traverseIdCons (x :: xs) (ys :: xss) = rewrite traverseIdCons xs xss in Refl
956+transposeCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> transpose (zipWith (::) xs xss) = xs :: transpose xss
957+transposeCons xs xss = rewrite zipWithIsLiftA2 Vect.(::) xs xss in rewrite transposeTraverse (pure (::) <*> xs <*> xss) in rewrite transposeTraverse xss in traverseIdCons xs xss
637--------------------------------------------------------------------------------
959--------------------------------------------------------------------------------
639--------------------------------------------------------------------------------
961--------------------------------------------------------------------------------
641−vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
642−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
644−vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
645−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
647implementation DecEq a => DecEq (Vect n a) where
963implementation DecEq a => DecEq (Vect n a) where
648 decEq [] [] = Yes Refl
964 decEq [] [] = Yes Refl
649 decEq (x :: xs) (y :: ys) with (decEq x y)
965 decEq (x :: xs) (y :: ys) with (decEq x y)