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.
(defmacro make-list (size &key initial-element)
(cons initial-element (cons 'nil 'nil)))))
(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)))))
- (repeat n x) creates a list of xes with length n; it
is a simpler alternative to make-list.
- Rewrite rule that eliminates make-list-ac (and hence make-list) in favor of repeat.
- Like make-list, but produces honses.