Idris2Doc : Data.Vect.Extra

Data.Vect.Extra

Additional functions about vectors
mapWithElem : (xs : Vectna) -> ((x : a) -> (0 _ : Elemxxs) -> b) -> Vectnb
  Version of `map` with runtime-irrelevant information that the
argument is an element of the vector

mapWithPos : (Finn -> a -> b) -> Vectna -> Vectnb
  Version of `map` with access to the current position