The submodule Vector allows safely manipulating indices into a vector.
type ('n, 'a) t = ('n, 'a) vectorlength is analogous to Array.length, but returns a cardinal instead of an ordinary integer.
get is Array.get, but expects an index instead of an ordinary integer. This guarantees that the index is within bounds.
set is Array.set, but expects an index instead of an ordinary integer. This guarantees that the index is within bounds.
set_cons t i x is short for set t i (x :: get t i).
val empty : (_, _) tempty is the empty vector.
make is analogous to Array.make. Invoking make n x fixes the cardinal n.
make' n f is roughly analogous to make n (f()), but removes the need to exhibit a value of type 'a when n is zero. The function call f() takes place only if n is greater than zero. It takes place at most once. Invoking make' n f fixes the cardinal n.
init is analogous to Array.init. Invoking init n f fixes the cardinal n.