		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-xor-lists

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

Definitions and Theorems

Function: 4vs-xor-lists

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