		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jfields-to-jcbody-elements

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

Signature
(jfields-to-jcbody-elements fields) → cbody-elements
Arguments: fields — Guard (jfield-listp fields).
Returns: cbody-elements — Type (jcbody-element-listp cbody-elements).

Definitions and Theorems

Function: jfields-to-jcbody-elements

(defun jfields-to-jcbody-elements (fields)
 (declare (xargs :guard (jfield-listp fields)))
 (let ((__function__ 'jfields-to-jcbody-elements))
  (declare (ignorable __function__))
  (cond
      ((endp fields) nil)
      (t (cons (jcbody-element-member (jcmember-field (car fields)))
               (jfields-to-jcbody-elements (cdr fields)))))))

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

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