Idris2Doc : Data.Vect.Extra

Data.Vect.Extra

Additional functions about vectors

mapWithElem : (xs : Vect n a) -> ((x : a) -> (0 _ : Elem x xs) -> b) -> Vect n b

  Version of `map` with runtime-irrelevant information that the
  argument is an element of the vector

mapWithPos : (Fin n -> a -> b) -> Vect n a -> Vect n b

  Version of `map` with access to the current position