Major Section: ACL2-BUILT-INS
List is the macro for building a list of objects. For example,
(list 5 6 7) returns a list of length 3 whose elements are
7 respectively. Also see list*.
List is defined in Common Lisp. See any Common Lisp documentation
for more information.