Idris2Doc : Data.Vect.Extra

Data.Vect.Extra

Additional functions about vectors

Definitions

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

Visibility: public export
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

Visibility: public export