		Search-engine friendly clone of the ACL2 documentation.

4vmask

4vmask-empty

(4vmask-empty x) recognizes the empty 4vmask.

Signature
(4vmask-empty x) → *
Arguments: x — Guard (4vmask-p x).

Definitions and Theorems

Function: 4vmask-empty$inline

(defun 4vmask-empty$inline (x)
  (declare (xargs :guard (4vmask-p x)))
  (let ((__function__ '4vmask-empty))
    (declare (ignorable __function__))
    (sparseint-equal (4vmask-fix x) 0)))