		Search-engine friendly clone of the ACL2 documentation.

Equal-by-eval-bdds

Max-depth

Depth of a cons tree.

Definitions and Theorems

Function: max-depth

(defun max-depth (x)
       (declare (xargs :guard t))
       (if (atom x)
           0
           (1+ (max (max-depth (car x))
                    (max-depth (cdr x))))))

Function: max-depth-memoize-condition

(defun max-depth-memoize-condition (x)
       (declare (ignorable x)
                (xargs :guard 't))
       (consp x))