make a list of a given size
Major Section:  PROGRAMMING

For a nonnegative integer size, (Make-list size) is a list of elements of length size, each of which is initialized to the :initial-element (which defaults to nil).

Make-list is a macro in ACL2, defined in terms of a tail recursive function make-list-ac whose guard requires size to be a nonnegative integer. Make-list is a Common Lisp function. See any Common Lisp documentation for more information.