		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

Seg-hidden-attri-alistp

Recognizer for pairs of segment register indices and values for the hidden portions containing the attr value of the registers.

Signature
(seg-hidden-attri-alistp alst) → *

Note that the register values are required to be n16p

Definitions and Theorems

Function: seg-hidden-attri-alistp

(defun seg-hidden-attri-alistp (alst)
  (declare (xargs :guard t))
  (let ((__function__ 'seg-hidden-attri-alistp))
    (declare (ignorable __function__))
    (if (atom alst)
        (equal alst nil)
      (if (atom (car alst))
          nil
        (let ((index (caar alst))
              (value (cdar alst))
              (rest (cdr alst)))
          (and (natp index)
               (< index 6)
               (unsigned-byte-p 16 value)
               (seg-hidden-attri-alistp rest)))))))