		Search-engine friendly clone of the ACL2 documentation.

Setp

Recognizer for sets.

Signature
(setp x) → *

Time complexity: O(n^2) (Note: the current implementation is inefficient. This should eventually be O(n) once we introduce a more efficient binary search tree property check via an mbe.)

Definitions and Theorems

Function: setp

(defun setp (x)
  (declare (xargs :type-prescription (booleanp (setp x))))
  (declare (xargs :guard t))
  (let ((__function__ 'setp))
    (declare (ignorable __function__))
    (and (binary-tree-p x)
         (bst-p x)
         (heapp x))))