		Search-engine friendly clone of the ACL2 documentation.

Pick-a-point

All-predicate

Signature
(all-predicate set) → *
Arguments: set — Guard (setp set).

Definitions and Theorems

Function: all-predicate

(defun all-predicate (set)
  (declare (xargs :guard (setp set)))
  (or (emptyp set)
      (and (set-predicate (head set))
           (all-predicate (left set))
           (all-predicate (right set)))))