Major Section: ACL2-BUILT-INS
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.