		Search-engine friendly clone of the ACL2 documentation.

Jenkins-hash

Jenkins-acc-symbol

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

Definitions and Theorems

Function: jenkins-acc-symbol$inline

(defun jenkins-acc-symbol$inline (symbol acc)
 (declare
   (type symbol symbol)
   (type (unsigned-byte 32) acc)
   (xargs :type-prescription (natp (jenkins-acc-symbol symbol acc)))
   (optimize (speed 3) (safety 0)))
 (declare (xargs :guard t))
 (the (unsigned-byte 32)
      (jenkins-acc-string
           (symbol-name symbol)
           (jenkins-acc-string (symbol-package-name symbol)
                               acc))))

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

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