		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-fix

Signature
(tree-fix tree) → tree$
Arguments: tree — Guard (binary-tree-p tree).
Returns: tree$ — Type (binary-tree-p tree$).

Definitions and Theorems

Function: tree-fix$inline

(defun tree-fix$inline (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (mbe :logic (if (binary-tree-p tree) tree nil)
       :exec (the (or cons null) tree)))

Theorem: binary-tree-p-of-tree-fix

(defthm binary-tree-p-of-tree-fix
  (b* ((tree$ (tree-fix$inline tree)))
    (binary-tree-p tree$))
  :rule-classes :rewrite)