		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-node

Construct a nonempty binary-tree.

Signature
(tree-node head left right) → tree
Arguments: left — Guard (binary-tree-p left).; right — Guard (binary-tree-p right).
Returns: tree — Type (binary-tree-p tree).

Definitions and Theorems

Function: tree-node$inline

(defun tree-node$inline (head left right)
 (declare (xargs :guard (and (binary-tree-p left)
                             (binary-tree-p right))))
 (declare
     (xargs :type-prescription (consp (tree-node head left right))))
 (list* head (tree-fix left)
        (tree-fix right)))

Theorem: binary-tree-p-of-tree-node

(defthm binary-tree-p-of-tree-node
  (b* ((tree (tree-node$inline head left right)))
    (binary-tree-p tree))
  :rule-classes :rewrite)