		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-character

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

Definitions and Theorems

Function: jenkins-acc-character$inline

(defun jenkins-acc-character$inline (c acc)
 (declare
     (type character c)
     (type (unsigned-byte 32) acc)
     (xargs :type-prescription (natp (jenkins-acc-character c acc)))
     (optimize (speed 3) (safety 0)))
 (declare (xargs :guard t))
 (the (unsigned-byte 32)
      (jenkins-acc-byte (the (unsigned-byte 8) (char-code c))
                        acc)))

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

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