		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

Ctri-alistp

Recognizer for pairs of control register indices and values.

Signature
(ctri-alistp alst) → *

Note that the register values are required to be n64p

Definitions and Theorems

Function: ctri-alistp

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