		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-induct

Induct over the structure of a binary tree.

Signature
(tree-induct tree) → *

Definitions and Theorems

Function: tree-induct

(defun tree-induct (tree)
  (declare (xargs :guard t))
  (or (tree-emptyp tree)
      (let ((left (tree-induct (tree-left tree)))
            (right (tree-induct (tree-right tree))))
        (declare (ignore left right))
        t)))