		Search-engine friendly clone of the ACL2 documentation.

4vmask

4veclist-mask?

Signature
(4veclist-mask? masks care dontcare) → *
Arguments: masks — Guard (4vmasklist-p masks).; care — Guard (4veclist-p care).; dontcare — Guard (4veclist-p dontcare).

Definitions and Theorems

Function: 4veclist-mask?

(defun 4veclist-mask? (masks care dontcare)
  (declare (xargs :guard (and (4vmasklist-p masks)
                              (4veclist-p care)
                              (4veclist-p dontcare))))
  (declare (xargs :guard (and (equal (len masks) (len care))
                              (equal (len masks) (len dontcare)))))
  (let ((__function__ '4veclist-mask?))
    (declare (ignorable __function__))
    (if (atom masks)
        nil
      (cons (4vec-mask? (car masks)
                        (car care)
                        (car dontcare))
            (4veclist-mask? (cdr masks)
                            (cdr care)
                            (cdr dontcare))))))