array 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def a.u == 1of(2of(a))

is mentioned by

Thm* T:Type, a:[T]Array , i:{a.l..a.u}. a[i T[array_el_wf]
Thm* i:j:{i...}, a:[T]Array{i..j}. a.l = i & a.u = j[p_array_properties]
Def arr1 @ arr2 == <arr1.l,arr2.u,(i.if i<arr1.u arr1[i] ; arr2[i] fi)>[array_append]
Def a[++i] == <(a.l+i),(a.u+i),(j.a[(j-i)])>[array_shift]
Def [T]Array{i..j} == {a:[T]Array | a.l = i & a.u = j }[p_array]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

array 1 Sections StandardLIB Doc