		Search-engine friendly clone of the ACL2 documentation.

Delete

Remove a value from the set.

Time complexity: O(\log(n)).

Definitions and Theorems

Function: delete1$inline

(defun delete1$inline (x set)
  (declare (xargs :guard (setp set)))
  (declare
       (xargs :type-prescription (or (consp (delete1 x set))
                                     (equal (delete1 x set) nil))))
  (tree-delete x (sfix set)))

Theorem: setp-of-delete1

(defthm setp-of-delete1
  (b* ((set$ (delete1$inline x set)))
    (setp set$))
  :rule-classes :rewrite)

Function: delete-macro-loop

(defun delete-macro-loop (list)
  (declare (xargs :guard (true-listp list)))
  (declare (xargs :guard (and (consp list) (consp (rest list)))))
  (if (endp (rest (rest list)))
      (list 'delete1
            (first list)
            (second list))
    (list 'delete1
          (first list)
          (delete-macro-loop (rest list)))))