		Search-engine friendly clone of the ACL2 documentation.

To-list

Create a list of values from a set.

Function: to-list

(defun to-list (set)
  (declare (xargs :guard (setp set)))
  (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)