		Search-engine friendly clone of the ACL2 documentation.

Lhrange

Lhrange-p

Recognizer for lhrange structures.

Signature
(lhrange-p x) → *

Definitions and Theorems

Function: lhrange-p

(defun lhrange-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'lhrange-p))
    (declare (ignorable __function__))
    (and (or (and (consp x)
                  (integerp (car x))
                  (not (eql (car x) 1)))
             (lhatom-p x))
         (b* ((w (if (and (consp x) (integerp (car x)))
                     (car x)
                   1))
              (atom (if (and (consp x) (integerp (car x)))
                        (cdr x)
                      x)))
           (and (posp w) (lhatom-p atom))))))