Idris2Doc : Data.Vect.Properties.Tabulate

Data.Vect.Properties.Tabulate

Tabulation gives a bijection between functions `f : Fin n -> a`
(up to extensional equality) and vectors `tabulate f : Vect n a`.
emptyInitial : (v : Vect0a) -> v = []
  The empty vector represents the unique function `Fin 0 -> a`

indexTabulate : (f : (Finn -> a)) -> (i : Finn) -> indexi (tabulatef) = fi
  Taking an index amounts to applying the tabulated function

tabulateExtensional : (f : (Finn -> a)) -> (g : (Finn -> a)) -> ((i : Finn) -> fi = gi) -> tabulatef = tabulateg
  Extensionally equivalent functions tabulate to the same vector

vectorExtensionality : (xs : Vectna) -> (ys : Vectna) -> ((i : Finn) -> indexixs = indexiys) -> xs = ys
  Vectors are uniquely determined by their elements