@@ -45,36 +45,64 @@ lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl
4545--------------------------------------------------------------------------------
4646
4747||| All but the first element of the vector
48+|||
49+||| ```idris example
50+||| tail [1,2,3,4]
51+||| ```
4852tail : Vect (S len) elem -> Vect len elem
4953tail (x::xs) = xs
5054
5155||| Only the first element of the vector
56+|||
57+||| ```idris example
58+||| head [1,2,3,4]
59+||| ```
5260head : Vect (S len) elem -> elem
5361head (x::xs) = x
5462
5563||| The last element of the vector
64+|||
65+||| ```idris example
66+||| last [1,2,3,4]
67+||| ```
5668last : Vect (S len) elem -> elem
5769last (x::[]) = x
5870last (x::y::ys) = last $ y::ys
5971
6072||| All but the last element of the vector
73+|||
74+||| ```idris example
75+||| init [1,2,3,4]
76+||| ```
6177init : Vect (S len) elem -> Vect len elem
6278init (x::[]) = []
6379init (x::y::ys) = x :: init (y::ys)
6480
6581||| Extract a particular element from a vector
82+|||
83+||| ```idris example
84+||| index 1 [1,2,3,4]
85+||| ```
6686index : Fin len -> Vect len elem -> elem
6787index FZ (x::xs) = x
6888index (FS k) (x::xs) = index k xs
6989
7090
7191||| Insert an element at a particular index
92+|||
93+||| ```idris example
94+||| insertAt 1 8 [1,2,3,4]
95+||| ```
7296insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem
7397insertAt FZ y xs = y :: xs
7498insertAt (FS k) y (x::xs) = x :: insertAt k y xs
7599insertAt (FS k) y [] = absurd k
76100
77101||| Construct a new vector consisting of all but the indicated element
102+|||
103+||| ```idris example
104+||| deleteAt 1 [1,2,3,4]
105+||| ```
78106deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem
79107deleteAt FZ (x::xs) = xs
80108deleteAt {len = S m} (FS k) (x::xs) = x :: deleteAt k xs
@@ -82,6 +110,10 @@ deleteAt {len = Z} (FS k) (x::xs) = absurd k
82110deleteAt _ [] impossible
83111
84112||| Replace an element at a particlar index with another
113+|||
114+||| ```idris example
115+||| replaceAt 1 8 [1,2,3,4]
116+||| ```
85117replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem
86118replaceAt FZ y (x::xs) = y :: xs
87119replaceAt (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
90122||| @ i the index to replace at
91123||| @ f the update function
92124||| @ xs the vector to replace in
125+|||
126+||| ```idris example
127+||| updateAt 1 (+10) [1,2,3,4]
128+||| ```
93129updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem
94130updateAt FZ f (x::xs) = f x :: xs
95131updateAt (FS k) f (x::xs) = x :: updateAt k f xs
@@ -100,18 +136,30 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
100136
101137||| Get the first n elements of a Vect
102138||| @ n the number of elements to take
139+|||
140+||| ```idris example
141+||| take 2 [1,2,3,4]
142+||| ```
103143take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
104144take Z xs = []
105145take (S k) (x :: xs) = x :: take k xs
106146
107147||| Remove the first n elements of a Vect
108148||| @ n the number of elements to remove
149+|||
150+||| ```idris example
151+||| drop 2 [1,2,3,4]
152+||| ```
109153drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
110154drop Z xs = xs
111155drop (S k) (x :: xs) = drop k xs
112156
113157||| Take up to the first n elements of a Vect if they exist.
114158||| @ n the maximum number of elements to take
159+|||
160+||| ```idris example
161+||| takeUpto 10 [1,2,3,4]
162+||| ```
115163takeUpto : (x : Nat) -> Vect n elem -> Vect (minimum x n) elem
116164takeUpto Z ys = []
117165takeUpto x [] = rewrite minimumZeroZeroLeft x in []
@@ -119,6 +167,10 @@ takeUpto (S x) (y::ys) = y :: takeUpto x ys
119167
120168||| Drop up to the first n elements of a Vect if they exist.
121169||| @ n the maximum number of elements to remove.
170+|||
171+||| ```idris example
172+||| dropUpto 10 [1,2,3,4]
173+||| ```
122174dropUpto : (x : Nat) -> Vect n elem -> Vect (n `minus` minimum x n) elem
123175dropUpto Z ys {n} = rewrite minusZeroRight n in ys
124176dropUpto x [] = []
@@ -128,6 +180,10 @@ dropUpto (S x) (y :: ys) = dropUpto x ys
128180||| Boolean predicate.
129181|||
130182||| @ p the predicate
183+|||
184+||| ```idris example
185+||| takeWhile (<3) [1,2,3,4]
186+||| ```
131187takeWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
132188takeWhile p [] = (_ ** [])
133189takeWhile p (x::xs) =
@@ -141,6 +197,10 @@ takeWhile p (x::xs) =
141197||| Boolean predicate.
142198|||
143199||| @ p the predicate
200+|||
201+||| ```idris example
202+||| dropWhile (<3) [1,2,3,4]
203+||| ```
144204dropWhile : (p : elem -> Bool) -> Vect len elem -> (q ** Vect q elem)
145205dropWhile p [] = (_ ** [])
146206dropWhile p (x::xs) =
@@ -154,6 +214,10 @@ dropWhile p (x::xs) =
154214--------------------------------------------------------------------------------
155215
156216||| Reverse the order of the elements of a vector
217+|||
218+||| ```idris example
219+||| reverse [1,2,3,4]
220+||| ```
157221reverse : Vect len elem -> Vect len elem
158222reverse xs = go [] xs
159223 where go : Vect n elem -> Vect m elem -> Vect (n+m) elem
@@ -164,6 +228,10 @@ reverse xs = go [] xs
164228||| Alternate an element between the other elements of a vector
165229||| @ sep the element to intersperse
166230||| @ xs the vector to separate with `sep`
231+|||
232+||| ```idris example
233+||| intersperse 0 [1,2,3,4]
234+||| ```
167235intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem
168236intersperse sep [] = []
169237intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -188,6 +256,10 @@ fromList' {len} ys (x::xs) =
188256||| Convert a list to a vector.
189257|||
190258||| The length of the list should be statically known.
259+|||
260+||| ```idris example
261+||| fromList [1,2,3,4]
262+||| ```
191263fromList : (l : List elem) -> Vect (length l) elem
192264fromList l =
193265 rewrite (sym $ plusZeroRightNeutral (length l)) in
@@ -198,6 +270,10 @@ fromList l =
198270--------------------------------------------------------------------------------
199271
200272||| Append two vectors
273+|||
274+||| ```idris example
275+||| [1,2,3,4] ++ [5,6]
276+||| ```
201277(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem
202278(++) [] ys = ys
203279(++) (x::xs) ys = x :: xs ++ ys
@@ -206,11 +282,19 @@ fromList l =
206282|||
207283||| @ len the number of times to repeat it
208284||| @ x the value to repeat
285+|||
286+||| ```idris example
287+||| replicate 4 1
288+||| ```
209289replicate : (len : Nat) -> (x : elem) -> Vect len elem
210290replicate Z x = []
211291replicate (S k) x = x :: replicate k x
212292
213293||| Merge two ordered vectors
294+|||
295+||| ```idris example
296+||| mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])
297+||| ```
214298mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem
215299mergeBy order [] [] = []
216300mergeBy order [] (x :: xs) = x :: xs
@@ -234,30 +318,54 @@ merge = mergeBy compare
234318||| @ f the function to combine elements with
235319||| @ xs the first vector of elements
236320||| @ ys the second vector of elements
321+|||
322+||| ```idris example
323+||| zipWith (+) (fromList [1,2,3,4]) (fromList [5,6,7,8])
324+||| ```
237325zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
238326zipWith f [] [] = []
239327zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
240328
241329||| Combine three equal-length vectors into a vector with some function
330+|||
331+||| ```idris example
332+||| zipWith3 (\x,y,z => x+y+z) (fromList [1,2,3,4]) (fromList [5,6,7,8]) (fromList [1,1,1,1])
333+||| ```
242334zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d
243335zipWith3 f [] [] [] = []
244336zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
245337
246338||| Combine two equal-length vectors pairwise
339+|||
340+||| ```idris example
341+||| zip (fromList [1,2,3,4]) (fromList [1,2,3,4])
342+||| ```
247343zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)
248344zip = zipWith (\x,y => (x,y))
249345
250346||| Combine three equal-length vectors elementwise into a vector of tuples
347+|||
348+||| ```idris example
349+||| zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])
350+||| ```
251351zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)
252352zip3 = zipWith3 (\x,y,z => (x,y,z))
253353
254354||| Convert a vector of pairs to a pair of vectors
355+|||
356+||| ```idris example
357+||| unzip (fromList [(1,2), (1,2)])
358+||| ```
255359unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)
256360unzip [] = ([], [])
257361unzip ((l, r)::xs) with (unzip xs)
258362 | (lefts, rights) = (l::lefts, r::rights)
259363
260364||| Convert a vector of three-tuples to a triplet of vectors
365+|||
366+||| ```idris example
367+||| unzip3 (fromList [(1,2,3), (1,2,3)])
368+||| ```
261369unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)
262370unzip3 [] = ([], [], [])
263371unzip3 ((l,c,r)::xs) with (unzip3 xs)
@@ -299,6 +407,10 @@ implementation Functor (Vect n) where
299407|||
300408||| @ f the partial function (expressed by returning `Maybe`)
301409||| @ xs the vector to check for results
410+|||
411+||| ```idris example
412+||| mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])
413+||| ```
302414mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)
303415mapMaybe f [] = (_ ** [])
304416mapMaybe f (x::xs) =
@@ -323,16 +435,28 @@ implementation Foldable (Vect n) where
323435--------------------------------------------------------------------------------
324436
325437||| Flatten a vector of equal-length vectors
438+|||
439+||| ```idris example
440+||| concat [[1,2,3], [4,5,6]]
441+||| ```
326442concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem
327443concat [] = []
328444concat (v::vs) = v ++ concat vs
329445
330446||| Foldr without seeding the accumulator
447+|||
448+||| ```idris example
449+||| foldr1 (-) (fromList [1,2,3])
450+||| ```
331451foldr1 : (t -> t -> t) -> Vect (S n) t -> t
332452foldr1 f [x] = x
333453foldr1 f (x::y::xs) = f x (foldr1 f (y::xs))
334454
335455||| Foldl without seeding the accumulator
456+|||
457+||| ```idris example
458+||| foldl1 (-) (fromList [1,2,3])
459+||| ```
336460foldl1 : (t -> t -> t) -> Vect (S n) t -> t
337461foldl1 f (x::xs) = foldl f x xs
338462
@@ -342,6 +466,10 @@ foldl1 f (x::xs) = foldl f x xs
342466
343467||| The scanl function is similar to foldl, but returns all the intermediate
344468||| accumulator states in the form of a vector.
469+|||
470+||| ```idris example
471+||| scanl (-) 0 (fromList [1,2,3])
472+||| ```
345473scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res
346474scanl f q [] = [q]
347475scanl f q (x::xs) = q :: scanl f (f q x) xs
@@ -350,6 +478,10 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
350478||| starting value.
351479||| It assumes the first element of the vector to be the starting value and then
352480||| starts the fold with the element following it.
481+|||
482+||| ```idris example
483+||| scanl1 (-) (fromList [1,2,3])
484+||| ```
353485scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem
354486scanl1 f [] = []
355487scanl1 f (x::xs) = scanl f x xs
@@ -362,6 +494,10 @@ scanl1 f (x::xs) = scanl f x xs
362494||| @ p the equality test
363495||| @ e the item to search for
364496||| @ xs the vector to search in
497+|||
498+||| ```idris example
499+||| elemBy (==) 2 [1,2,3,4]
500+||| ```
365501elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool
366502elemBy p e [] = False
367503elemBy p e (x::xs) = p e x || elemBy p e xs
@@ -369,17 +505,29 @@ elemBy p e (x::xs) = p e x || elemBy p e xs
369505||| Use the default Boolean equality on elements to search for an item
370506||| @ x what to search for
371507||| @ xs where to search
508+|||
509+||| ```idris example
510+||| elem 3 [1,2,3,4]
511+||| ```
372512elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool
373513elem = elemBy (==)
374514
375515||| Find the association of some key with a user-provided comparison
376516||| @ p the comparison operator for keys (True if they match)
377517||| @ e the key to look for
518+|||
519+||| ```idris example
520+||| lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]
521+||| ```
378522lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val
379523lookupBy p e [] = Nothing
380524lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
381525
382526||| Find the assocation of some key using the default Boolean equality test
527+|||
528+||| ```idris example
529+||| lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]
530+||| ```
383531lookup : Eq key => key -> Vect n (key, val) -> Maybe val
384532lookup = lookupBy (==)
385533
@@ -387,11 +535,19 @@ lookup = lookupBy (==)
387535||| @ p the comparison operator
388536||| @ elems the vector to search
389537||| @ xs what to search for
538+|||
539+||| ```idris example
540+||| hasAnyBy (==) [2,5] [1,2,3,4]
541+||| ```
390542hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool
391543hasAnyBy p elems [] = False
392544hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
393545
394546||| Check if any element of xs is found in elems using the default Boolean equality test
547+|||
548+||| ```idris example
549+||| hasAny [2,5] [1,2,3,4]
550+||| ```
395551hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool
396552hasAny = hasAnyBy (==)
397553
@@ -401,30 +557,62 @@ hasAny = hasAnyBy (==)
401557
402558||| Find the first element of the vector that satisfies some test
403559||| @ p the test to satisfy
560+|||
561+||| ```idris example
562+||| find (== 3) [1,2,3,4]
563+||| ```
404564find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem
405565find p [] = Nothing
406566find p (x::xs) = if p x then Just x else find p xs
407567
408568||| Find the index of the first element of the vector that satisfies some test
569+|||
570+||| ```idris example
571+||| findIndex (== 3) [1,2,3,4]
572+||| ```
409573findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)
410574findIndex p [] = Nothing
411575findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
412576
413577||| Find the indices of all elements that satisfy some test
578+|||
579+||| ```idris example
580+||| findIndices (< 3) [1,2,3,4]
581+||| ```
414582findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)
415583findIndices p [] = []
416584findIndices p (x :: xs) = let is = map FS $ findIndices p xs
417585 in if p x then 0 :: is else is
418586
587+||| Find the index of the first element of the vector that satisfies some test
588+|||
589+||| ```idris example
590+||| elemIndexBy (==) 3 [1,2,3,4]
591+||| ```
419592elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)
420593elemIndexBy p e = findIndex $ p e
421594
595+||| Find the index of the first element of the vector equal to the given one.
596+|||
597+||| ```idris example
598+||| elemIndex 3 [1,2,3,4]
599+||| ```
422600elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)
423601elemIndex = elemIndexBy (==)
424602
603+||| Find the indices of all elements that satisfy some test
604+|||
605+||| ```idris example
606+||| elemIndicesBy (<=) 3 [1,2,3,4]
607+||| ```
425608elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)
426609elemIndicesBy p e = findIndices $ p e
427610
611+||| Find the indices of all elements uquals to the given one
612+|||
613+||| ```idris example
614+||| elemIndices 3 [1,2,3,4,3]
615+||| ```
428616elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)
429617elemIndices = elemIndicesBy (==)
430618
@@ -433,6 +621,10 @@ elemIndices = elemIndicesBy (==)
433621--------------------------------------------------------------------------------
434622
435623||| Find all elements of a vector that satisfy some test
624+|||
625+||| ```idris example
626+||| filter (< 3) (fromList [1,2,3,4])
627+||| ```
436628filter : (elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
437629filter p [] = ( _ ** [] )
438630filter p (x::xs) =
@@ -443,6 +635,10 @@ filter p (x::xs) =
443635 (_ ** tail)
444636
445637||| Make the elements of some vector unique by some test
638+|||
639+||| ```idris example
640+||| nubBy (==) (fromList [1,2,2,3,4,4])
641+||| ```
446642nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p ** Vect p elem)
447643nubBy = nubBy' []
448644 where
@@ -454,15 +650,29 @@ nubBy = nubBy' []
454650 | (_ ** tail) = (_ ** x::tail)
455651
456652||| Make the elements of some vector unique by the default Boolean equality
653+|||
654+||| ```idris example
655+||| nub (fromList [1,2,2,3,4,4])
656+||| ```
457657nub : Eq elem => Vect len elem -> (p ** Vect p elem)
458658nub = nubBy (==)
459659
660+||| Delete first element from list according to some test
661+|||
662+||| ```idris example
663+||| deleteBy (<) 3 (fromList [1,2,2,3,4,4])
664+||| ```
460665deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p ** Vect p elem)
461666deleteBy _ _ [] = (_ ** [])
462667deleteBy eq x (y::ys) =
463668 let (len ** zs) = deleteBy eq x ys
464669 in if x `eq` y then (_ ** ys) else (S len ** y ::zs)
465670
671+||| Delete first element from list equal to the given one
672+|||
673+||| ```idris example
674+||| delete 2 (fromList [1,2,2,3,4,4])
675+||| ```
466676delete : (Eq elem) => elem -> Vect len elem -> (p ** Vect p elem)
467677delete = deleteBy (==)
468678
@@ -477,11 +687,21 @@ delete = deleteBy (==)
477687|||
478688||| @ n the index to split at
479689||| @ xs the `Vect` to split in two
690+|||
691+||| ```idris example
692+||| splitAt 2 (fromList [1,2,3,4])
693+||| ```
480694splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
481695splitAt Z xs = ([], xs)
482696splitAt (S k) (x :: xs) with (splitAt k xs)
483697 | (tk, dr) = (x :: tk, dr)
484698
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.
701+|||
702+||| ```idris example
703+||| partition (== 2) (fromList [1,2,3,2,4])
704+||| ```
485705partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
486706partition p [] = ((_ ** []), (_ ** []))
487707partition p (x::xs) =
@@ -495,17 +715,37 @@ partition p (x::xs) =
495715-- Predicates
496716--------------------------------------------------------------------------------
497717
718+||| Verify vector prefix
719+|||
720+||| ```idris example
721+||| isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])
722+||| ```
498723isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
499724isPrefixOfBy p [] right = True
500725isPrefixOfBy p left [] = False
501726isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
502727
728+||| Verify vector prefix
729+|||
730+||| ```idris example
731+||| isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])
732+||| ```
503733isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
504734isPrefixOf = isPrefixOfBy (==)
505735
736+||| Verify vector suffix
737+|||
738+||| ```idris example
739+||| isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])
740+||| ```
506741isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool
507742isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)
508743
744+||| Verify vector suffix
745+|||
746+||| ```idris example
747+||| isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])
748+||| ```
509749isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool
510750isSuffixOf = isSuffixOfBy (==)
511751
@@ -513,10 +753,20 @@ isSuffixOf = isSuffixOfBy (==)
513753-- Conversions
514754--------------------------------------------------------------------------------
515755
756+||| Convert Maybe type into Vect
757+|||
758+||| ```idris example
759+||| maybeToVect (Just 2)
760+||| ```
516761maybeToVect : Maybe elem -> (p ** Vect p elem)
517762maybeToVect Nothing = (_ ** [])
518763maybeToVect (Just j) = (_ ** [j])
519764
765+||| Convert first element of Vect (if exists) into Maybe.
766+|||
767+||| ```idris example
768+||| vectToMaybe [2]
769+||| ```
520770vectToMaybe : Vect len elem -> Maybe elem
521771vectToMaybe [] = Nothing
522772vectToMaybe (x::xs) = Just x
@@ -525,6 +775,11 @@ vectToMaybe (x::xs) = Just x
525775-- Misc
526776--------------------------------------------------------------------------------
527777
778+||| Filter out Nothings from Vect
779+|||
780+||| ```idris example
781+||| catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]
782+||| ```
528783catMaybes : Vect n (Maybe elem) -> (p ** Vect p elem)
529784catMaybes [] = (_ ** [])
530785catMaybes (Nothing::xs) = catMaybes xs
@@ -532,6 +787,11 @@ catMaybes ((Just j)::xs) =
532787 let (_ ** tail) = catMaybes xs
533788 in (_ ** j::tail)
534789
790+||| Get diagonal elements
791+|||
792+||| ```idris example
793+||| diag [[1,2,3], [4,5,6], [7,8,9]]
794+||| ```
535795diag : Vect len (Vect len elem) -> Vect len elem
536796diag [] = []
537797diag ((x::xs)::xss) = x :: diag (map tail xss)
@@ -545,6 +805,10 @@ range {len=S _} = FZ :: map FS range
545805||| This is like zipping all the inner `Vect`s together and is equivalent to `traverse id` (`transposeTraverse`).
546806|||
547807||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
808+|||
809+||| ```idris example
810+||| transpose [[1,2], [3,4], [5,6], [7,8]]
811+||| ```
548812transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)
549813transpose [] = replicate _ [] -- = [| [] |]
550814transpose (x :: xs) = zipWith (::) x (transpose xs) -- = [| x :: xs |]