Selected Objects
| COM | ARRAY_DEFS |
[T]Array : type of all arrays of type T.[T]Array{i..j-} : Those arrays with start index i and end index j-1. e.g. a[i], a[i+1], ..., a[j-1]NIL |
| def | array |
[T]Array == n:  m:{n...}{n..m }  T |
| def | array_lb |
a.l == 1of(a) |
| def | array_ub |
a.u == 1of(2of(a)) |
| def | p_array |
[T]Array{i..j} == {a:[T]Array | a.l = i & a.u = j } |
| THM | p_array_properties |
 i:, j:{i...}, a:[T]Array{i..j}. a.l = i & a.u = j |
| def | array_el |
a[i] == 2of(2of(a))(i) |
| def | array_seg |
a[i..j] == <i,j,2of(2of(a))> |
| def | array_shift |
a[++i] == <(a.l+i),(a.u+i),( j.a[(j-i)])> |
| def | array_append |
arr1 @ arr2 == <arr1.l,arr2.u,(i.if i<arr1.u arr1[i] ; arr2[i] fi)> |