		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$inline

(defun insert1$inline (x set)
  (declare (xargs :guard (setp set)))
  (tree-insert x (sfix set)))

Theorem: setp-of-insert1

(defthm setp-of-insert1
  (b* ((set$ (insert1$inline 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)))))
  (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.