Idris2Doc : Data.Vect.Properties.Index

Data.Vect.Properties.Index

Properties of Data.Vect.index
indexNaturality : (i : Finn) -> (f : (a -> b)) -> (xs : Vectna) -> indexi (mapfxs) = f (indexixs)
  `index i : Vect n a -> a` is a natural transformation

indexRange : (i : Finn) -> indexirange = i
  `range` tabulates the identity function (by definition)

indexReplicate : (i : Finn) -> (x : a) -> indexi (replicatenx) = x
  Replication tabulates the constant function

indexTranspose : (xss : Vectm (Vectna)) -> (i : Finn) -> indexi (transposexss) = map (indexi) xss
  The `i`-th vector in a transposed matrix is the vector of `i`-th components

recallElem : Elemxxs -> a
  Recall an element by its position, as we may not have the element
at runtime

recallElemSpec : (pos : Elemxxs) -> recallElempos = x
  Recalling by a position of `x` does yield `x`