		Search-engine friendly clone of the ACL2 documentation.

Insert

Add a value (or multiples values) to the set.

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

Definitions and Theorems

Function: insert1

(defun insert1 (x set)
  (declare (xargs :guard (setp set)))
  (let ((__function__ 'insert1))
    (declare (ignorable __function__))
    (tree-insert x (sfix set))))

Theorem: setp-of-insert1

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

Function: insert-macro-loop

(defun insert-macro-loop (list)
  (declare (xargs :guard (true-listp list)))
  (declare (xargs :guard (and (consp list) (consp (rest list)))))
  (let ((__function__ 'insert-macro-loop))
    (declare (ignorable __function__))
    (if (endp (rest (rest list)))
        (list 'insert1
              (first list)
              (second list))
      (list 'insert1
            (first list)
            (insert-macro-loop (rest list))))))

Subtopics

Insert-all: Add a list of values to the set.