		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

Unsigned-4vec-p

Signature
(unsigned-4vec-p n x) → *
Arguments: n — Guard (natp n).

Definitions and Theorems

Function: unsigned-4vec-p

(defun unsigned-4vec-p (n x)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'unsigned-4vec-p))
    (declare (ignorable __function__))
    (and (4vec-p x)
         (unsigned-byte-p n (4vec->upper x))
         (unsigned-byte-p n (4vec->lower x)))))