array
1
Doc
Def
[T]Array{i..j
} == {a:[T]Array | a.l = i & a.u = j}
Thm*
array_append_wf
Thm*
array_shift_wf
Thm*
array_seg_wf
Thm*
array_el_wfp
Thm*
p_array_properties