		Search-engine friendly clone of the ACL2 documentation.

Implementation

Heap<

A total order based on object hashes.

Signature
(heap< x y) → *

This order is determined primarily by the hash values of objects. Since the hashes may collide, we fall back to << when the hashes are equal to ensure the order is total.

The goal of this order is to be largely uncorrelated with <<. Therefore, it is important that the hash function (jenkins-hash) does not collide frequently and exhibits a strong avalanche effect.

Function: heap<$inline

(defun heap<$inline (x y)
  (declare (xargs :type-prescription (booleanp (heap< x y)))
           (optimize (speed 3) (safety 0)))
  (declare (xargs :guard t))
  (let ((hash-x (hash x)) (hash-y (hash y)))
    (declare (type (unsigned-byte 32) hash-x)
             (type (unsigned-byte 32) hash-y))
    (heap<-with-hashes x y hash-x hash-y)))

Macro: heap<

(defmacro heap< (x y)
  (list 'heap<$inline x y))

Subtopics

Heap<-with-hashes: Variant of heap< which uses pre-computed hashes.