		Search-engine friendly clone of the ACL2 documentation.

Ienv

Ienvp

Recognizer for ienv structures.

Signature
(ienvp x) → *

Definitions and Theorems

Function: ienvp

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

Theorem: consp-when-ienvp

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