- (++) : HVect ts ->
HVect us ->
HVect (ts ++
us)
Append two HVect
s.
- Fixity
- Left associative, precedence 7
- 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
- interface Shows
- shows : Shows ts =>
HVect ts ->
Vect k
String
- deleteAt : (i : Fin (S l)) ->
HVect us ->
HVect (deleteAt i
us)
- get : HVect ts ->
{auto p : Elem t
ts} ->
t
Extract an arbitrary element of the correct type.
- t
the goal type
- hvectInjective1 : (x ::
xs =
y ::
ys) ->
x =
y
- hvectInjective2 : (x ::
xs =
y ::
ys) ->
xs =
ys
- index : (i : Fin k) ->
HVect ts ->
index i
ts
Extract an element from an HVect
- put : t ->
HVect ts ->
{auto p : Elem t
ts} ->
HVect ts
Replace an element with the correct type.
- replaceAt : (i : Fin k) ->
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.
- updateAt : (i : Fin k) ->
(index i
ts ->
t) ->
HVect ts ->
HVect (replaceAt i
t
ts)