		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation

Atj-post-translate-jcbody-elements

Post-translate a list of Java class body elements.

Signature
(atj-post-translate-jcbody-elements elems) → new-elems
Arguments: elems — Guard (jcbody-element-listp elems).
Returns: new-elems — Type (jcbody-element-listp new-elems).

For now this consists of a single operation, but it may be extended in the future.

Definitions and Theorems

Function: atj-post-translate-jcbody-elements

(defun atj-post-translate-jcbody-elements (elems)
  (declare (xargs :guard (jcbody-element-listp elems)))
  (let ((__function__ 'atj-post-translate-jcbody-elements))
    (declare (ignorable __function__))
    (atj-cache-const-methods elems)))

Theorem: jcbody-element-listp-of-atj-post-translate-jcbody-elements

(defthm jcbody-element-listp-of-atj-post-translate-jcbody-elements
  (b* ((new-elems (atj-post-translate-jcbody-elements elems)))
    (jcbody-element-listp new-elems))
  :rule-classes :rewrite)