		Search-engine friendly clone of the ACL2 documentation.

Vl-linecol

Vl-linecol-p

Recognizer for vl-linecol structures.

Signature
(vl-linecol-p x) → *

Definitions and Theorems

Function: vl-linecol-p

(defun vl-linecol-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'vl-linecol-p))
    (declare (ignorable __function__))
    (if (integerp x)
        (and (<= 0 x)
             (< 0 (ash x -22))
             (< x (expt 2 52)))
      (and (consp x)
           (posp (car x))
           (natp (cdr x))
           (or (<= (expt 2 30) (car x))
               (<= (expt 2 22) (cdr x)))))))