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`.

Definitions

vectorExtensionality : (xs : Vect n a) -> (ys : Vect n a) -> ((i : Fin n) -> index i xs = index i ys) -> xs = ys

  Vectors are uniquely determined by their elements

Visibility: export

tabulateExtensional : (f : (Fin n -> a)) -> (g : (Fin n -> a)) -> ((i : Fin n) -> f i = g i) -> tabulate f = tabulate g

  Extensionally equivalent functions tabulate to the same vector

Visibility: export

indexTabulate : (f : (Fin n -> a)) -> (i : Fin n) -> index i (tabulate f) = f i

  Taking an index amounts to applying the tabulated function

Visibility: export

emptyInitial : (v : Vect 0 a) -> v = []

  The empty vector represents the unique function `Fin 0 -> a`

Visibility: export