		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex3-byte1-equiv-under-mask

Signature
(vex3-byte1-equiv-under-mask vex3byte1 vex3byte11 mask) → *
Arguments: vex3byte1 — Guard (vex3-byte1-p vex3byte1).; vex3byte11 — Guard (vex3-byte1-p vex3byte11).; mask — Guard (integerp mask).

Definitions and Theorems

Function: vex3-byte1-equiv-under-mask$inline

(defun vex3-byte1-equiv-under-mask$inline
       (vex3byte1 vex3byte11 mask)
  (declare (xargs :guard (and (vex3-byte1-p vex3byte1)
                              (vex3-byte1-p vex3byte11)
                              (integerp mask))))
  (fty::int-equiv-under-mask (vex3-byte1-fix vex3byte1)
                             (vex3-byte1-fix vex3byte11)
                             mask))