		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-true-list

Signature
(jenkins-acc-true-list list acc) → acc$
Arguments: list — Guard (true-listp list).
Returns: acc$ — Type (unsigned-byte-p 32 acc$).

Definitions and Theorems

Function: jenkins-acc-true-list

(defun jenkins-acc-true-list (list acc)
  (declare (xargs :guard (true-listp list)))
  (declare (type (or cons null) list)
           (type (unsigned-byte 32) acc)
           (optimize (speed 3) (safety 0)))
  (let ((acc (mbe :logic (if (unsigned-byte-p 32 acc) acc 0)
                  :exec acc)))
    (if (endp list)
        acc
      (let ((first (first list)))
        (if (consp first)
            (jenkins-acc-true-list (list* (car first)
                                          (cdr first)
                                          (rest list))
                                   (jenkins-acc-byte 112 acc))
          (jenkins-acc-true-list (rest list)
                                 (jenkins-acc-atom first acc)))))))

Theorem: return-type-of-jenkins-acc-true-list

(defthm return-type-of-jenkins-acc-true-list
  (b* ((acc$ (jenkins-acc-true-list list acc)))
    (unsigned-byte-p 32 acc$))
  :rule-classes :rewrite)