		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jmethods-to-jcbody-elements

Lift the composition of jcmember-method followed by jcbody-element-member to lists.

Signature
(jmethods-to-jcbody-elements methods) → cbody-elements
Arguments: methods — Guard (jmethod-listp methods).
Returns: cbody-elements — Type (jcbody-element-listp cbody-elements).

Definitions and Theorems

Function: jmethods-to-jcbody-elements

(defun jmethods-to-jcbody-elements (methods)
 (declare (xargs :guard (jmethod-listp methods)))
 (let ((__function__ 'jmethods-to-jcbody-elements))
  (declare (ignorable __function__))
  (cond
    ((endp methods) nil)
    (t (cons (jcbody-element-member (jcmember-method (car methods)))
             (jmethods-to-jcbody-elements (cdr methods)))))))

Theorem: jcbody-element-listp-of-jmethods-to-jcbody-elements

(defthm jcbody-element-listp-of-jmethods-to-jcbody-elements
  (b* ((cbody-elements (jmethods-to-jcbody-elements methods)))
    (jcbody-element-listp cbody-elements))
  :rule-classes :rewrite)