from vectors import Vectors
| Operation Name | Input Type | Output Type | Faults | Description |
|---|
| add | AddRequest | Vector | - | Adds an element to the end of a vector. |
| concat | VectorPair | Vector | - | Concatenates two vectors. |
| equals | VectorPair | bool | - | Checks if two vectors are deeply equal (all elements of the two vectors must be respectively deeply equal). |
| insert | InsertRequest | Vector | - | Inserts an element at the specified index. The rest of the vector is shifted to the right. |
| slice | SliceRequest | Vector | - | Slices the vector from an index to another. |
AddRequest:
void {
item[1,1]: undefined //
vector[1,1]: Vector //
}
InsertRequest:
void {
item[1,1]: undefined //
index[1,1]: int //
vector[1,1]: Vector //
}
SliceRequest:
void {
from[1,1]: int //
vector[1,1]: Vector //
to[1,1]: int //
}
|void {
vector[1,1]: Vector //
to[1,1]: int //
}
|void {
from[1,1]: int //
vector[1,1]: Vector //
}
Vector:
void {
items[0,1]: undefined //
}
VectorPair:
void {
fst[1,1]: Vector //
snd[1,1]: Vector //
}