		Search-engine friendly clone of the ACL2 documentation.

Set-induct

Induct over the structure of a set.

Signature
(set-induct set) → *

Definitions and Theorems

Function: set-induct

(defun set-induct (set)
  (declare (xargs :guard t))
  (or (emptyp set)
      (let ((left (set-induct (left set)))
            (right (set-induct (right set))))
        (declare (ignore left right))
        t)))