		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jblock-ifelse

Build a block consisting of a single Java if-else statement.

Signature
(jblock-ifelse test then else) → block
Arguments: test — Guard (jexprp test).; then — Guard (jblockp then).; else — Guard (jblockp else).
Returns: block — Type (jblockp block).

Definitions and Theorems

Function: jblock-ifelse

(defun jblock-ifelse (test then else)
  (declare (xargs :guard (and (jexprp test)
                              (jblockp then)
                              (jblockp else))))
  (let ((__function__ 'jblock-ifelse))
    (declare (ignorable __function__))
    (list (jstatem-ifelse test then else))))

Theorem: jblockp-of-jblock-ifelse

(defthm jblockp-of-jblock-ifelse
  (b* ((block (jblock-ifelse test then else)))
    (jblockp block))
  :rule-classes :rewrite)