		Search-engine friendly clone of the ACL2 documentation.

Initialize-x86-state

Rgfi-alistp

Recognizer for pairs of general-purpose register indices and values.

Signature
(rgfi-alistp alst) → *

Note that the register values are required to be n64p, as opposed to i64p (which is what is required for !rgfi).

Definitions and Theorems

Function: rgfi-alistp

(defun rgfi-alistp (alst)
  (declare (xargs :guard t))
  (let ((__function__ 'rgfi-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
                  *64-bit-general-purpose-registers-len*)
               (unsigned-byte-p 64 value)
               (rgfi-alistp rest)))))))