		Search-engine friendly clone of the ACL2 documentation.

From-list

Create a set from a list of values.

This is just a wrapper around insert-all.

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

Function: from-list$inline

(defun from-list$inline (list)
  (declare (xargs :guard (true-listp list)))
  (insert-all list nil))

Theorem: setp-of-from-list

(defthm setp-of-from-list
  (b* ((set$ (from-list$inline list)))
    (setp set$))
  :rule-classes :rewrite)