		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jblock-locvar

Build a block consisting of a single (non-final) local variable declaration statement.

Signature
(jblock-locvar type name init?) → block
Arguments: type — Guard (jtypep type).; name — Guard (stringp name).; init? — Guard (maybe-jexprp init?).
Returns: block — Type (jblockp block).

Definitions and Theorems

Function: jblock-locvar

(defun jblock-locvar (type name init?)
  (declare (xargs :guard (and (jtypep type)
                              (stringp name)
                              (maybe-jexprp init?))))
  (let ((__function__ 'jblock-locvar))
    (declare (ignorable __function__))
    (list (jstatem-locvar (make-jlocvar :final? nil
                                        :type type
                                        :name name
                                        :init? init?)))))

Theorem: jblockp-of-jblock-locvar

(defthm jblockp-of-jblock-locvar
  (b* ((block (jblock-locvar type name init?)))
    (jblockp block))
  :rule-classes :rewrite)