		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jblock-do

Build a block consisting of a single Java do statement.

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

Definitions and Theorems

Function: jblock-do

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

Theorem: jblockp-of-jblock-do

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