		Search-engine friendly clone of the ACL2 documentation.

Implementation

Tree-nodes-count

The number of elements in a tree.

Signature
(tree-nodes-count tree) → *
Arguments: tree — Guard (binary-tree-p tree).

Definitions and Theorems

Function: tree-nodes-count

(defun tree-nodes-count (tree)
 (declare (xargs :guard (binary-tree-p tree)))
 (declare (xargs :type-prescription (natp (tree-nodes-count tree))))
 (let ((__function__ 'tree-nodes-count))
   (declare (ignorable __function__))
   (mbe :logic
        (if (tree-emptyp tree)
            0
          (+ 1 (tree-nodes-count (tree-left tree))
             (tree-nodes-count (tree-right tree))))
        :exec (fast-tree-nodes-count (list tree) 0))))