		Search-engine friendly clone of the ACL2 documentation.

Structures

Vex2-byte1-equiv-under-mask

Signature
(vex2-byte1-equiv-under-mask x x1 mask) → *
Arguments: x — Guard (vex2-byte1-p x).; x1 — Guard (vex2-byte1-p x1).; mask — Guard (integerp mask).

Definitions and Theorems

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

(defun vex2-byte1-equiv-under-mask$inline (x x1 mask)
  (declare (xargs :guard (and (vex2-byte1-p x)
                              (vex2-byte1-p x1)
                              (integerp mask))))
  (fty::int-equiv-under-mask (vex2-byte1-fix x)
                             (vex2-byte1-fix x1)
                             mask))