Higher order Arrays/Lists

Stream: lean4

[Robert]

Just a basic question, but in Lean is there a way to declare higher order lists/arrays? say a 3d array, how would I go about declaring it? Say I just want to create an array/list as below which is a 3d tensor (I know basic arrays and Matrix exists in Lean but cannot seem to generalize it)
a = [[[0], [0]]

Any pointers would be appreciated!

[Julian Berman]

That seems fine other than you have imbalanced parens and invalid assignment syntax :) -- but e.g.:

def a := [[[0], [0]]]

will compile. Whether you want Array, List, Vector, or other probably depends on what you want to do with that. (See also scilean possibly)

[Robert]

oh so i tried it and it declared it as a list, how would one go about doing it as an array? I just want to write manipulate some arrays and do some operations with them! Whats the best way on doing all of that?

[Kim Morrison]

def X : Array (Array Nat) := #[#[0], #[1]]
def Y : Vector (Vector Nat 1) 2 := #v[#v[0], #v[1]]