proc main(): void {
v := ["a", "b", "c"] // Str[3] — a static length, inferred
mut Str[dyn] w = ["a", "b"] // dynamic — the only kind append accepts
append(w, "c")
echo v[0] // a
echo v[0:1] // ["a", "b"] — both bounds inclusive
echo v[1:] // ["b", "c"]
echo v == ["a", "b", "c"] // true — element by element
Str[3][2] grid = [["a", "b", "c"], ["d", "e", "f"]]
echo grid[1][2] // f — two rows of three
}A vector holds elements of one type, side by side in memory, and its type says how long it is:
Str[3] is static: exactly three, always. v := ["a", "b", "c"] is one — a length read off the value is a length all the same.Str[dyn] is dynamic: it promises nothing about its length, and it is the only kind append, prepend and drop change. It has to be written out, as mut Str[dyn] v = ….Str[] is a parameter-only spelling that takes either kind.A vector of vectors reads left to right: Str[3][2] is two vectors of three, so grid[1][2] is the last cell of the second row. v[i] reads an element and v[lo:hi] slices with both bounds inclusive, so v[0:1] is two elements; either bound may be left out. Every index and slice is proved in range when the program compiles — the next slide is how. + joins two vectors into a new one, and == compares them element by element.