		Search-engine friendly clone of the ACL2 documentation.

Implementation

Hash

The hash function used by heap<.

Signature
(hash x) → hash
Returns: hash — Type (unsigned-byte-p 32 hash).

This is just a wrapper around jenkins-hash. This function is defined to allow us to easily switch hash functions if needed. To hash objects (e.g., for use with heap<-with-hashes), users should call this function instead of jenkins-hash.

Definitions and Theorems

Function: hash$inline

(defun hash$inline (x)
  (declare (xargs :type-prescription (natp (hash x))))
  (declare (xargs :guard t))
  (jenkins-hash x))

Theorem: return-type-of-hash

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