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))
(and (binary-tree-p x)
(bst-p x)
(heapp x)))
