IdrisDoc: Data.HVect

Data.HVect

updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)
update : (t -> u) -> HVect ts -> {auto p : Elem t 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 : t -> HVect ts -> {auto p : Elem t 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 : HVect ts -> {auto p : Elem t 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)
interface Shows 
shows : Shows 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