Data.Vect.Properties.Index

Properties of Data.Vect.index

Definitions

recallElem : Elem x xs -> a

  Recall an element by its position, as we may not have the element
  at runtime

Visibility: public export

recallElemSpec : (pos : Elem x xs) -> recallElem pos = x

  Recalling by a position of `x` does yield `x`

Visibility: export

indexNaturality : (i : Fin n) -> (f : (a -> b)) -> (xs : Vect n a) -> index i (map f xs) = f (index i xs)

  `index i : Vect n a -> a` is a natural transformation

Visibility: export

indexReplicate : (i : Fin n) -> (x : a) -> index i (replicate n x) = x

  Replication tabulates the constant function

Visibility: export

indexRange : (i : Fin n) -> index i range = i

  `range` tabulates the identity function (by definition)

Visibility: export

indexTranspose : (xss : Vect m (Vect n a)) -> (i : Fin n) -> index i (transpose xss) = map (index i) xss

  The `i`-th vector in a transposed matrix is the vector of `i`-th components

Visibility: export