Construction of Lists

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

[* *] : -> List

The empty list.

[* e_1, e_2, ..., e_n *] : Elt,.., Elt -> List

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