		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-ACL2-number

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

Definitions and Theorems

Function: jenkins-acc-acl2-number$inline

(defun jenkins-acc-acl2-number$inline (n acc)
 (declare
   (type number n)
   (type (unsigned-byte 32) acc)
   (xargs :type-prescription (natp (jenkins-acc-acl2-number n acc)))
   (optimize (speed 3) (safety 0)))
 (declare (xargs :guard t))
 (the (unsigned-byte 32)
      (cond ((integerp n)
             (jenkins-acc-integer (the signed-byte n)
                                  acc))
            ((rationalp n)
             (jenkins-acc-rational (the rational n)
                                   acc))
            (t (jenkins-acc-complex-rational (the complex n)
                                             acc)))))

Theorem: return-type-of-jenkins-acc-acl2-number

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