# Construction of Lists

Lists can be constructed by expressions enclosed in special brackets `[*` and `*]`.

## `[* *] -> List`

The empty list.

## `[* e₁, e₂, ..., eₙ *]: Elt, .., Elt -> List`

Given a list of expressions $e_1, \ldots, e_n$, defining elements $a_1, a_2, \ldots, a_n$, create the list containing $a_1, a_2, \ldots, a_n$.