		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-rational

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

Definitions and Theorems

Function: jenkins-acc-rational$inline

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

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

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