A | |
| apply [Mergeable_vector.Mergeable_vector] | apply a p applies the compatibe patch p on a.
|
D | |
| delete [Mergeable_vector.Vector] | delete v i deletes the element at position i in v.
|
| diff [Mergeable_vector.Mergeable_vector] | diff a b returns a patch p such that apply a p = b.
|
G | |
| get [Mergeable_vector.Vector] | get v i returns the element at position i in v.
|
I | |
| insert [Mergeable_vector.Vector] | insert v i e inserts the element e at position i in v.
|
L | |
| length [Mergeable_vector.Vector] |
Length of vector.
|
M | |
| merge [Mergeable_vector.Mergeable_vector] | merge r a l r performs a 3-way merge between two vectors l and r,
and their common ancestor a.
|
S | |
| set [Mergeable_vector.Vector] | set v i e updates the element at position i in v to e.
|