Array type implements a dynamic (aka growable) array.
It is defined as
namespace hidden structure Array (α : Type u) where data : List α end hidden
but its execution time representation is optimized, and it is similar to C++
std::vector<T> and Rust
The Lean type checker has no special support for reducing
You can create arrays in several ways. You can create a small array by listing consecutive values between
] and separated by commas, as shown in the following examples.
#check #[1, 2, 3] -- Array Nat #check # -- Array ?m
The type of the array elements is inferred from the literals used and must be consistent.
#check #["hello", "world"] -- Array String -- The following is not valid #check_failure #[10, "hello"]
Recall that the command
#check_failure <term> only succeeds when the given term is not type correct.
To create an array of size
n in which all the elements are initialized to some value
#eval mkArray 5 'a' -- #['a', 'a', 'a', 'a', 'a']
You can access array elements by using brackets (
def f (a : Array Nat) (i : Fin a.size) := a[i] + a[i]
Note that the index
i has type
Fin a.size, i.e., it is natural number less than
You can also write
def f (a : Array Nat) (i : Nat) (h : i < a.size) := a[i] + a[i]
The bracket operator is whitespace sensitive.
def f (xs : List Nat) : List Nat := xs ++ xs def as : Array Nat := #[1, 2, 3, 4] def idx : Fin 4 := 2 #eval f [1, 2, 3] -- This is a function application #eval as[idx] -- This is an array access
a[i] has two variants:
a[i]?. In both cases,
i has type
Nat. The first one
produces a panic error message if the index
i is out of bounds. The latter returns an
#eval #['a', 'b', 'c']? -- some 'b' #eval #['a', 'b', 'c']? -- none #eval #['a', 'b', 'c']! -- 'b!