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 Arrays.

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 ]).

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 a.size. 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 :=

#eval f [1, 2, 3] -- This is a function application

#eval as[idx] -- This is an array access

The notation a[i] has two variants: a[i]! and 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 Option type.

#eval #['a', 'b', 'c'][1]?
-- some 'b'
#eval #['a', 'b', 'c'][5]?
-- none
#eval #['a', 'b', 'c'][1]!
-- 'b!