		Search-engine friendly clone of the ACL2 documentation.

To-list

Create a list of values from a set.

Signature
(to-list set) → list
Arguments: set — Guard (setp set).
Returns: list — Type (true-listp list).

Definitions and Theorems

Function: to-list

(defun to-list (set)
  (declare (xargs :guard (setp set)))
  (let ((__function__ 'to-list))
    (declare (ignorable __function__))
    (tree-post-order (sfix set))))

Theorem: true-listp-of-to-list

(defthm true-listp-of-to-list
  (b* ((list (to-list set)))
    (true-listp list))
  :rule-classes :rewrite)