		Search-engine friendly clone of the ACL2 documentation.

Jfield

Jfieldp

Recognizer for jfield structures.

Signature
(jfieldp x) → *

Definitions and Theorems

Function: jfieldp

(defun jfieldp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'jfieldp))
  (declare (ignorable __function__))
  (and
   (mbe :logic
        (and (alistp x)
             (equal (strip-cars x)
                    '(access static? final?
                             transient? volatile? type name init?)))
        :exec (fty::alist-with-carsp
                   x
                   '(access static? final?
                            transient? volatile? type name init?)))
   (b* ((access (cdr (std::da-nth 0 x)))
        (static? (cdr (std::da-nth 1 x)))
        (final? (cdr (std::da-nth 2 x)))
        (transient? (cdr (std::da-nth 3 x)))
        (volatile? (cdr (std::da-nth 4 x)))
        (type (cdr (std::da-nth 5 x)))
        (name (cdr (std::da-nth 6 x)))
        (init? (cdr (std::da-nth 7 x))))
     (and (jaccessp access)
          (booleanp static?)
          (booleanp final?)
          (booleanp transient?)
          (booleanp volatile?)
          (jtypep type)
          (stringp name)
          (maybe-jexprp init?))))))

Theorem: consp-when-jfieldp

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