		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

(defun delete1 (x set)
  (declare (xargs :guard (setp set)))
  (declare
       (xargs :type-prescription (or (consp (delete1 x set))
                                     (equal (delete1 x set) nil))))
  (let ((__function__ 'delete1))
    (declare (ignorable __function__))
    (tree-delete x (sfix set))))

Theorem: setp-of-delete1

(defthm setp-of-delete1
  (b* ((set$ (delete1 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)))))
  (let ((__function__ 'delete-macro-loop))
    (declare (ignorable __function__))
    (if (endp (rest (rest list)))
        (list 'delete1
              (first list)
              (second list))
      (list 'delete1
            (first list)
            (delete-macro-loop (rest list))))))