		Search-engine friendly clone of the ACL2 documentation.

Setting-up-page-tables

Physical-addr-qword-alistp

Recognizer for a list of pairs of up to 52-bit wide physical address and byte.

Signature
(physical-addr-qword-alistp alst) → *

Definitions and Theorems

Function: physical-addr-qword-alistp

(defun physical-addr-qword-alistp (alst)
  (declare (xargs :guard t))
  (let ((__function__ 'physical-addr-qword-alistp))
    (declare (ignorable __function__))
    (if (atom alst)
        (equal alst nil)
      (if (atom (car alst))
          nil
        (let ((addr (caar alst))
              (qword (cdar alst))
              (rest (cdr alst)))
          (and (integerp addr)
               (<= 0 addr)
               (< addr 4503599627370489)
               (n64p qword)
               (physical-addr-qword-alistp rest)))))))