Construction of Lists

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

[* *] : -> List

The empty list.

[* e₁, e₂, ..., e_n *] : Elt,.., Elt -> List

Given a list of expressions e₁, ..., e_n, defining elements a₁, a₂, ..., a_n, create the list containing a₁, a₂, ..., a_n.