Data.Setoid.Vect.Functional

The setoid of vectors over a given setoid, defined using a function

Definitions

0 .VectEquality : (a : Setoid) -> Rel (Vect n (U a))

Totality: total
Visibility: public export

index : (i : Fin n) -> a .VectEquality xs ys -> (a .equivalence) .relation (index i xs) (index i ys)

Totality: total
Visibility: export

VectSetoid : Nat -> Setoid -> Setoid

Totality: total
Visibility: public export

VectMap : (a ~~> b) ~> (VectSetoid n a ~~> VectSetoid n b)

Totality: total
Visibility: public export