		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-or-lists

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

Definitions and Theorems

Function: 4vs-or-lists

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