0 | ||| Additional functions about vectors
 1 | module Data.Vect.Extra
 2 |
 3 | import Data.Vect
 4 | import Data.Fin
 5 | import Data.Vect.Elem
 6 |
 7 | ||| Version of `map` with access to the current position
 8 | public export
 9 | mapWithPos : (f : Fin n -> a -> b) -> Vect n a -> Vect n b
10 | mapWithPos f [] = []
11 | mapWithPos f (x :: xs) = f 0 x :: mapWithPos (f . FS) xs
12 |
13 | ||| Version of `map` with runtime-irrelevant information that the
14 | ||| argument is an element of the vector
15 | public export
16 | mapWithElem : (xs : Vect n a)
17 |   -> (f : (x : a) -> (0 pos : x `Elem` xs) -> b)
18 |   -> Vect n b
19 | mapWithElem []        f = []
20 | mapWithElem (x :: xs) f
21 |   = f x Here :: mapWithElem xs
22 |                 (\x,pos => f x (There pos))
23 |