Make-list
Make a list of a given size
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.
Macro: make-list
(defmacro make-list (size &key initial-element)
(cons 'make-list-ac
(cons size (cons initial-element '(nil)))))
Function: make-list-ac
(defun make-list-ac (n val ac)
(declare (xargs :guard (and (integerp n) (>= n 0))))
(cond ((zp n) ac)
(t (make-list-ac (1- n)
val (cons val ac)))))Subtopics
- Repeat
- (repeat n x) creates a list of xes with length n; it
is a simpler alternative to make-list.
- Make-list-ac-removal
- Rewrite rule that eliminates make-list-ac (and hence make-list) in favor of repeat.
- Hons-make-list
- Like make-list, but produces honses.
