Array literals are written in curly plus square brackets, with two levels of square brackets for two-dimensional arrays. Examples: {[[], []]} (an empty array with two rows and zero columns ), integerArray {[[1, 2, 3], [4, 5, 6]]} (two rows and three columns of integers, uses integerArray Integers), stringArray {[["a"], ["b"]]} (two rows and one column of strings, uses stringArray Character strings)
The generic sort of a two-dimensional array containing elements of sort 𝕊 is Array2D(𝕊), with s:𝕊, Array2D(s) ⊆ Array. The sort of an array of known size is Array(𝕊, ℕ.nz, ℕ.nz), with s:𝕊, i1:ℕ.nz, i2:ℕ.nz, Array(s, i1, i2) ⊆ Array2D(s).
An empty two-dimensional array has sort EmptyArray(ℕ, ℕ). An empty array cannot have a regular array sort, because regular array sorts depend on the type of the array elements. An empty array has no elements. The integer arguments in the array sort define the size of the array. At least one of them must be zero, otherwise the array would not be empty. An empty two-dimensional array of unknown size has sort EmptyArray2D, with i1:ℕ, i2:ℕ, EmptyArray(i1, i2) ⊆ EmptyArray2D and EmptyArray2D ⊆ Array.