		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Binary-tree-p

Recognizer for binary-trees.

Signature
(binary-tree-p x) → *

Definitions and Theorems

Function: binary-tree-p

(defun binary-tree-p (x)
  (declare (xargs :type-prescription (booleanp (binary-tree-p x))))
  (declare (xargs :guard t))
  (let ((__function__ 'binary-tree-p))
    (declare (ignorable __function__))
    (or (null x)
        (and (consp x)
             (consp (cdr x))
             (binary-tree-p (cadr x))
             (binary-tree-p (cddr x))))))