		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

Seg-visiblei-alistp

Recognizer for pairs of segment register indices and values for the visible portions of the registers.

Signature
(seg-visiblei-alistp alst) → *

Note that the register values are required to be n16p

Definitions and Theorems

Function: seg-visiblei-alistp

(defun seg-visiblei-alistp (alst)
  (declare (xargs :guard t))
  (let ((__function__ 'seg-visiblei-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 *segment-register-names-len*)
               (unsigned-byte-p 16 value)
               (seg-visiblei-alistp rest)))))))