		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jexpr-literal-floating

Build a Java expression consisting of a floating-point literal.

Signature
(jexpr-literal-floating value) → expr
Arguments: value — Guard (natp value).
Returns: expr — Type (jexprp expr).

Definitions and Theorems

Function: jexpr-literal-floating

(defun jexpr-literal-floating (value)
  (declare (xargs :guard (natp value)))
  (let ((__function__ 'jexpr-literal-floating))
    (declare (ignorable __function__))
    (jexpr-literal (jliteral-floating value))))

Theorem: jexprp-of-jexpr-literal-floating

(defthm jexprp-of-jexpr-literal-floating
  (b* ((expr (jexpr-literal-floating value)))
    (jexprp expr))
  :rule-classes :rewrite)