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

Definitions

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

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

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

Visibility: export
emptyInitial : (v : Vect0a) ->v= []
  The empty vector represents the unique function `Fin 0 -> a`

Visibility: export