		Search-engine friendly clone of the ACL2 documentation.

Jmethod

Jmethodp

Recognizer for jmethod structures.

Signature
(jmethodp x) → *

Definitions and Theorems

Function: jmethodp

(defun jmethodp (x)
 (declare (xargs :guard t))
 (let ((__function__ 'jmethodp))
  (declare (ignorable __function__))
  (and
    (mbe :logic
         (and (alistp x)
              (equal (strip-cars x)
                     '(access abstract? static?
                              final? synchronized? native? strictfp?
                              result name params throws body)))
         :exec (fty::alist-with-carsp
                    x
                    '(access abstract? static?
                             final? synchronized? native? strictfp?
                             result name params throws body)))
    (b* ((access (cdr (std::da-nth 0 x)))
         (abstract? (cdr (std::da-nth 1 x)))
         (static? (cdr (std::da-nth 2 x)))
         (final? (cdr (std::da-nth 3 x)))
         (synchronized? (cdr (std::da-nth 4 x)))
         (native? (cdr (std::da-nth 5 x)))
         (strictfp? (cdr (std::da-nth 6 x)))
         (result (cdr (std::da-nth 7 x)))
         (name (cdr (std::da-nth 8 x)))
         (params (cdr (std::da-nth 9 x)))
         (throws (cdr (std::da-nth 10 x)))
         (body (cdr (std::da-nth 11 x))))
      (and (jaccessp access)
           (booleanp abstract?)
           (booleanp static?)
           (booleanp final?)
           (booleanp synchronized?)
           (booleanp native?)
           (booleanp strictfp?)
           (jresultp result)
           (stringp name)
           (jparam-listp params)
           (string-listp throws)
           (jblockp body))))))

Theorem: consp-when-jmethodp

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