Data.HVect

updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)

update : {auto p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)

Update an element with the correct type.

replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)

put : {auto p : Elem t ts} -> t -> HVect ts -> HVect ts

Replace an element with the correct type.

index : (i : Fin k) -> HVect ts -> index i ts

Extract an element from an HVect

hvectInjective2 : (x :: xs = y :: ys) -> xs = ys

hvectInjective1 : (x :: xs = y :: ys) -> x = y

get : {auto p : Elem t ts} -> HVect ts -> t

Extract an arbitrary element of the correct type.

t

the goal type

deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)

class Shows 

shows : Shows k ts => HVect ts -> Vect k String

data HVect : Vect k Type -> Type

Heterogeneous vectors where the type index gives, element-wise,
the types of the contents.

Nil : HVect []

(::) : t -> HVect ts -> HVect (t :: ts)

Fixity

Left associative, precedence 7

(++) : HVect ts -> HVect us -> HVect (ts ++ us)

Append two HVects.

Fixity

Left associative, precedence 7