		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

Gdtr/idtrbits-equiv-under-mask

Signature
(gdtr/idtrbits-equiv-under-mask x x1 mask) → *
Arguments: x — Guard (gdtr/idtrbits-p x).; x1 — Guard (gdtr/idtrbits-p x1).; mask — Guard (integerp mask).

Definitions and Theorems

Function: gdtr/idtrbits-equiv-under-mask

(defun gdtr/idtrbits-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (gdtr/idtrbits-p x)
                              (gdtr/idtrbits-p x1)
                              (integerp mask))))
  (let ((__function__ 'gdtr/idtrbits-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (gdtr/idtrbits-fix x)
                               (gdtr/idtrbits-fix x1)
                               mask)))