		Search-engine friendly clone of the ACL2 documentation.

Char+short+int+long+llong+bool-format

Char+short+int+long+llong+bool-formatp

Recognizer for char+short+int+long+llong+bool-format structures.

Signature
(char+short+int+long+llong+bool-formatp x) → *

Definitions and Theorems

Function: char+short+int+long+llong+bool-formatp

(defun char+short+int+long+llong+bool-formatp (x)
 (declare (xargs :guard t))
 (and
    (mbe :logic
         (and (alistp x)
              (equal (strip-cars x)
                     '(uchar schar char short int long llong bool)))
         :exec (fty::alist-with-carsp
                    x
                    '(uchar schar char short int long llong bool)))
    (b* ((uchar (cdr (std::da-nth 0 x)))
         (schar (cdr (std::da-nth 1 x)))
         (char (cdr (std::da-nth 2 x)))
         (short (cdr (std::da-nth 3 x)))
         (int (cdr (std::da-nth 4 x)))
         (long (cdr (std::da-nth 5 x)))
         (llong (cdr (std::da-nth 6 x)))
         (bool (cdr (std::da-nth 7 x))))
      (and (uchar-formatp uchar)
           (schar-formatp schar)
           (char-formatp char)
           (integer-formatp short)
           (integer-formatp int)
           (integer-formatp long)
           (integer-formatp llong)
           (bool-formatp bool)))))

Theorem: consp-when-char+short+int+long+llong+bool-formatp

(defthm consp-when-char+short+int+long+llong+bool-formatp
  (implies (char+short+int+long+llong+bool-formatp x)
           (consp x))
  :rule-classes :compound-recognizer)