		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-node-with-hint

A variant of tree-node which uses cons-with-hint.

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

Definitions and Theorems

Function: tree-node-with-hint$inline

(defun tree-node-with-hint$inline (head left right hint)
  (declare (xargs :guard (and (binary-tree-p left)
                              (binary-tree-p right)
                              (binary-tree-p hint))))
  (declare
       (xargs :type-prescription
              (consp (tree-node-with-hint head left right hint))))
  (cons-with-hint head
                  (cons-with-hint (tree-fix left)
                                  (tree-fix right)
                                  (cdr hint))
                  hint))

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

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