		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-integer

Signature
(jenkins-acc-integer n acc) → acc$
Returns: acc$ — Type (unsigned-byte-p 32 acc$).

Definitions and Theorems

Function: jenkins-acc-integer$inline

(defun jenkins-acc-integer$inline (n acc)
  (declare
       (type signed-byte n)
       (type (unsigned-byte 32) acc)
       (xargs :type-prescription (natp (jenkins-acc-integer n acc)))
       (optimize (speed 3) (safety 0)))
  (declare (xargs :guard t))
  (the (unsigned-byte 32)
       (if (natp n)
           (jenkins-acc-nat n acc)
         (jenkins-acc-nat (the unsigned-byte (- n))
                          (jenkins-acc-byte 0 acc)))))

Theorem: return-type-of-jenkins-acc-integer

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