		Search-engine friendly clone of the ACL2 documentation.

Integer-format

Integer-formatp

Recognizer for integer-format structures.

Signature
(integer-formatp x) → *

Definitions and Theorems

Function: integer-formatp

(defun integer-formatp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'integer-formatp))
  (declare (ignorable __function__))
  (and
     (mbe :logic (and (alistp x)
                      (equal (strip-cars x) '(pair)))
          :exec (fty::alist-with-carsp x '(pair)))
     (b* ((pair (cdr (std::da-nth 0 x))))
       (and (uinteger+sinteger-formatp pair)
            (uinteger-sinteger-bit-roles-wfp
                 (uinteger-format->bits
                      (uinteger+sinteger-format->unsigned pair))
                 (sinteger-format->bits
                      (uinteger+sinteger-format->signed pair))))))))

Theorem: consp-when-integer-formatp

(defthm consp-when-integer-formatp
  (implies (integer-formatp x) (consp x))
  :rule-classes :compound-recognizer)