		Search-engine friendly clone of the ACL2 documentation.

Sparseint$

Sparseint$-p

Recognizer for sparseint$ structures.

Signature
(sparseint$-p x) → *

Definitions and Theorems

Function: sparseint$-p

(defun sparseint$-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'sparseint$-p))
    (declare (ignorable __function__))
    (cond ((atom x) (b* ((val x)) (integerp val)))
          (t (and (consp (cdr x))
                  (integerp (car x))
                  (b* ((width (logtail 2 (car x)))
                       (lsbs-taller (logbitp 0 (car x)))
                       (msbs-taller (logbitp 1 (car x)))
                       (lsbs (cadr x))
                       (msbs (cddr x)))
                    (and (posp width)
                         (booleanp lsbs-taller)
                         (booleanp msbs-taller)
                         (sparseint$-p lsbs)
                         (sparseint$-p msbs))))))))