		Search-engine friendly clone of the ACL2 documentation.

Segmentation-bitstructs

System-segment-descriptor-attributesbits-equiv-under-mask

Signature
(system-segment-descriptor-attributesbits-equiv-under-mask x x1 mask) → *
Arguments: x — Guard (system-segment-descriptor-attributesbits-p x).; x1 — Guard (system-segment-descriptor-attributesbits-p x1).; mask — Guard (integerp mask).

Definitions and Theorems

Function: system-segment-descriptor-attributesbits-equiv-under-mask

(defun system-segment-descriptor-attributesbits-equiv-under-mask
       (x x1 mask)
 (declare
  (xargs :guard (and (system-segment-descriptor-attributesbits-p x)
                     (system-segment-descriptor-attributesbits-p x1)
                     (integerp mask))))
 (let
  ((__function__
        'system-segment-descriptor-attributesbits-equiv-under-mask))
  (declare (ignorable __function__))
  (fty::int-equiv-under-mask
       (system-segment-descriptor-attributesbits-fix x)
       (system-segment-descriptor-attributesbits-fix x1)
       mask)))