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