		Search-engine friendly clone of the ACL2 documentation.

Bst<

Bst<-with-hashes

Variant of bst< which may use pre-computed hashes.

Signature
(bst<-with-hashes x y hash-x hash-y) → *

This is currently a dummy function warpping bst<. It is provided in case we wish to change the order to make use of hash values, as heap< currently does.

Definitions and Theorems

Function: bst<-with-hashes$inline

(defun bst<-with-hashes$inline (x y hash-x hash-y)
  (declare (xargs :type-prescription
                  (booleanp (bst<-with-hashes x y hash-x hash-y)))
           (ignore hash-x hash-y))
  (declare (xargs :guard t))
  (bst< x y))