		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jblock-locvar-final

Build a block consisting of a single final local variable declaration statement.

Signature
(jblock-locvar-final 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-final

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

Theorem: jblockp-of-jblock-locvar-final

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