		Search-engine friendly clone of the ACL2 documentation.

Ia32e-paging

Find-similar-paging-entries-from-page-present-equality-aux

Signature
(find-similar-paging-entries-from-page-present-equality-aux index entry-var calls) → *
Arguments: index — Guard (natp index).

Definitions and Theorems

Function: find-similar-paging-entries-from-page-present-equality-aux

(defun find-similar-paging-entries-from-page-present-equality-aux
       (index entry-var calls)
 (declare (xargs :guard (natp index)))
 (let
  ((__function__
       'find-similar-paging-entries-from-page-present-equality-aux))
  (declare (ignorable __function__))
  (if (atom calls)
      nil
    (b* ((one-call (car calls))
         ((unless (and (true-listp one-call)
                       (true-listp (nth index one-call))
                       (equal (len (nth index one-call)) 2)))
          nil))
      (cons (list (cons entry-var (nth 1 (nth index one-call))))
            (find-similar-paging-entries-from-page-present-equality-aux
                 index entry-var (cdr calls)))))))