		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-atom

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

Definitions and Theorems

Function: jenkins-acc-atom$inline

(defun jenkins-acc-atom$inline (x acc)
  (declare (type atom x)
           (type (unsigned-byte 32) acc)
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard t))
  (the (unsigned-byte 32)
       (cond ((symbolp x) (jenkins-acc-symbol x acc))
             ((acl2-numberp x)
              (jenkins-acc-acl2-number x acc))
             ((stringp x) (jenkins-acc-string x acc))
             ((characterp x)
              (jenkins-acc-character x acc))
             (t (mbe :logic (if (unsigned-byte-p 32 acc) acc 0)
                     :exec acc)))))

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

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