		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Tree-emptyp

Check if a binary-tree is empty.

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

Definitions and Theorems

Function: tree-emptyp$inline

(defun tree-emptyp$inline (tree)
  (declare (xargs :guard (binary-tree-p tree)))
  (declare (xargs :type-prescription (booleanp (tree-emptyp tree))))
  (endp (tree-fix tree)))