		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-in-order

Create an in-order list of values from a tree.

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

Definitions and Theorems

Function: tree-in-order

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

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

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