		Search-engine friendly clone of the ACL2 documentation.

List*

Build a list

List* is the Common Lisp macro for building a list of objects from given elements and a tail. For example, (list* 5 6 '(7 8 9)) equals the list '(5 6 7 8 9). Also see list.

List* is a Common Lisp function. See any Common Lisp documentation for more information.

Macro: list*

(defmacro list* (&rest args)
          (declare (xargs :guard (consp args)))
          (list*-macro args))

Function: list*-macro

(defun list*-macro (lst)
       (declare (xargs :guard (and (true-listp lst) (consp lst))))
       (if (endp (cdr lst))
           (car lst)
           (cons 'cons
                 (cons (car lst)
                       (cons (list*-macro (cdr lst)) nil)))))