		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-and-lists

(4vs-and-lists x y) pairwise ands together the sexprs from two separate lists, forming a new sexpr list.

Definitions and Theorems

Function: 4vs-and-lists

(defun 4vs-and-lists (x y)
  (declare (xargs :guard (equal (len x) (len y))))
  (if (atom x)
      nil
    (cons (4vs-and (car x) (car y))
          (4vs-and-lists (cdr x) (cdr y)))))