		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jblock-smethod

Build a block consisting of a single Java static method call.

Signature
(jblock-smethod type name args) → block
Arguments: type — Guard (jtypep type).; name — Guard (stringp name).; args — Guard (jexpr-listp args).
Returns: block — Type (jblockp block).

Definitions and Theorems

Function: jblock-smethod

(defun jblock-smethod (type name args)
  (declare (xargs :guard (and (jtypep type)
                              (stringp name)
                              (jexpr-listp args))))
  (let ((__function__ 'jblock-smethod))
    (declare (ignorable __function__))
    (jblock-expr (jexpr-smethod type name args))))

Theorem: jblockp-of-jblock-smethod

(defthm jblockp-of-jblock-smethod
  (b* ((block (jblock-smethod type name args)))
    (jblockp block))
  :rule-classes :rewrite)