		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-pre-order

Create a pre-order list of values from a tree.

Signature
(tree-pre-order tree) → list
Arguments: tree — Guard (binary-tree-p tree).
Returns: list — Type (true-listp list).

Definitions and Theorems

Function: tree-pre-order

(defun tree-pre-order (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (let ((__function__ 'tree-pre-order))
    (declare (ignorable __function__))
    (if (tree-emptyp tree)
        nil
      (cons (tree-head tree)
            (append (tree-pre-order (tree-left tree))
                    (tree-pre-order (tree-right tree)))))))

Theorem: true-listp-of-tree-pre-order

(defthm true-listp-of-tree-pre-order
  (b* ((list (tree-pre-order tree)))
    (true-listp list))
  :rule-classes :rewrite)