		Search-engine friendly clone of the ACL2 documentation.

Insert

Insert-all

Add a list of values to the set.

Signature
(insert-all list set) → set$
Arguments: list — Guard (true-listp list).; set — Guard (setp set).
Returns: set$ — Type (setp set$).

Time complexity: O(n\log(n+m)), where n is the size of the list, and m is the size of the set.

Definitions and Theorems

Function: insert-all

(defun insert-all (list set)
  (declare (xargs :guard (and (true-listp list) (setp set))))
  (let ((__function__ 'insert-all))
    (declare (ignorable __function__))
    (if (endp list)
        (sfix set)
      (insert-all (rest list)
                  (insert (first list) set)))))

Theorem: setp-of-insert-all

(defthm setp-of-insert-all
  (b* ((set$ (insert-all list set)))
    (setp set$))
  :rule-classes :rewrite)