		Search-engine friendly clone of the ACL2 documentation.

Binary-tree

Binary-tree-listp

Recognizer for a true list of binary trees.

Signature
(binary-tree-listp x) → *

Definitions and Theorems

Function: binary-tree-listp

(defun binary-tree-listp (x)
  (declare
       (xargs :type-prescription (booleanp (binary-tree-listp x))))
  (declare (xargs :guard t))
  (if (consp x)
      (and (binary-tree-p (first x))
           (binary-tree-listp (rest x)))
    (null x)))