		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jblock-asg-name

Build a block consisting of a single Java assignment where the left-hand side is a named expression.

Signature
(jblock-asg-name left right) → block
Arguments: left — Guard (stringp left).; right — Guard (jexprp right).
Returns: block — Type (jblockp block).

Definitions and Theorems

Function: jblock-asg-name

(defun jblock-asg-name (left right)
  (declare (xargs :guard (and (stringp left) (jexprp right))))
  (let ((__function__ 'jblock-asg-name))
    (declare (ignorable __function__))
    (jblock-expr (jexpr-binary (jbinop-asg)
                               (jexpr-name left)
                               right))))

Theorem: jblockp-of-jblock-asg-name

(defthm jblockp-of-jblock-asg-name
  (b* ((block (jblock-asg-name left right)))
    (jblockp block))
  :rule-classes :rewrite)