		Search-engine friendly clone of the ACL2 documentation.

Atj-common-code-generation

Atj-gen-jboolean

Generate Java code to build a Java boolean from an ACL2 boolean.

Signature
(atj-gen-jboolean boolean) → expr
Arguments: boolean — Guard (booleanp boolean).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: atj-gen-jboolean

(defun atj-gen-jboolean (boolean)
  (declare (xargs :guard (booleanp boolean)))
  (let ((__function__ 'atj-gen-jboolean))
    (declare (ignorable __function__))
    (if boolean (jexpr-literal-true)
      (jexpr-literal-false))))

Theorem: jexprp-of-atj-gen-jboolean

(defthm jexprp-of-atj-gen-jboolean
  (b* ((expr (atj-gen-jboolean boolean)))
    (jexprp expr))
  :rule-classes :rewrite)