		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jblock-expr

Build a block consisting of a single Java expression (as an expression statement.

Signature
(jblock-expr expr) → block
Arguments: expr — Guard (jexprp expr).
Returns: block — Type (jblockp block).

Definitions and Theorems

Function: jblock-expr

(defun jblock-expr (expr)
  (declare (xargs :guard (jexprp expr)))
  (let ((__function__ 'jblock-expr))
    (declare (ignorable __function__))
    (list (jstatem-expr expr))))

Theorem: jblockp-of-jblock-expr

(defthm jblockp-of-jblock-expr
  (b* ((block (jblock-expr expr)))
    (jblockp block))
  :rule-classes :rewrite)