		Search-engine friendly clone of the ACL2 documentation.

Lhatom

Lhatom-p

Recognizer for lhatom structures.

Signature
(lhatom-p x) → *

Definitions and Theorems

Function: lhatom-p

(defun lhatom-p (x)
 (declare (xargs :guard t))
 (let ((__function__ 'lhatom-p))
  (declare (ignorable __function__))
  (cond
   ((eq x :z) (b* nil t))
   (t
    (and (or (atom x)
             (and (eq (car x) :var) (svar-p x))
             (or (eq (car x) :z)
                 (not (eql 0 (cdr x)))))
         (b* ((name (if (or (atom x)
                            (and (eq (car x) :var) (consp (cdr x))))
                        x
                      (car x)))
              (rsh (if (or (atom x)
                           (and (eq (car x) :var) (consp (cdr x))))
                       0
                     (cdr x))))
           (and (svar-p name) (natp rsh))))))))