Arrays
The 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 Vec<T>
.
The Lean type checker has no special support for reducing Array
s.
You can create arrays in several ways. You can create a small array by listing consecutive values between
#[
and ]
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 a
, use mkArray
.
#eval mkArray 5 'a'
-- #['a', 'a', 'a', 'a', 'a']
Accessing elements
You can access array elements by using brackets ([
and ]
).
#eval #['a', 'b', 'c'][1]
-- 'b'
def getThird (xs : Array Nat) : Nat :=
xs[2]
#eval getThird #[10, 20, 30, 40]
-- 30
The bracket operator is whitespace sensitive.
def f (xs : List Nat) : List Nat :=
xs ++ xs
def as : Array Nat :=
#[1, 2, 3, 4]
#eval f [1, 2, 3] -- This is a function application
#eval as[2] -- This is an array access