		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jblock-for

Bulid a block consisting of a single Java for statement.

Signature
(jblock-for init test update body) → block
Arguments: init — Guard (jexprp init).; test — Guard (jexprp test).; update — Guard (jexprp update).; body — Guard (jblockp body).
Returns: block — Type (jblockp block).

Definitions and Theorems

Function: jblock-for

(defun jblock-for (init test update body)
  (declare (xargs :guard (and (jexprp init)
                              (jexprp test)
                              (jexprp update)
                              (jblockp body))))
  (let ((__function__ 'jblock-for))
    (declare (ignorable __function__))
    (list (jstatem-for init test update body))))

Theorem: jblockp-of-jblock-for

(defthm jblockp-of-jblock-for
  (b* ((block (jblock-for init test update body)))
    (jblockp block))
  :rule-classes :rewrite)