		Search-engine friendly clone of the ACL2 documentation.

Atj-java-abstract-syntax

Jliteral-long-dec-nouscores

Build a Java long literal in base 10 without underscores.

Signature
(jliteral-long-dec-nouscores value) → lit
Arguments: value — Guard (natp value).
Returns: lit — Type (jliteralp lit).

This is an integer decimal literal with the type suffix L. We use the uppercase type suffix, and not the lowercase one, as recommended in [JLS14:3.10.1].

Definitions and Theorems

Function: jliteral-long-dec-nouscores

(defun jliteral-long-dec-nouscores (value)
 (declare (xargs :guard (natp value)))
 (let ((__function__ 'jliteral-long-dec-nouscores))
  (declare (ignorable __function__))
  (b* ((codes (chars=>nats (str::nat-to-dec-chars value))))
   (jliteral-integer
    (integer-literal-dec
        (make-dec-integer-literal
             :digits/uscores (decdig/uscore-digit-list codes)
             :suffix? (optional-integer-type-suffix-uppercase)))))))

Theorem: jliteralp-of-jliteral-long-dec-nouscores

(defthm jliteralp-of-jliteral-long-dec-nouscores
  (b* ((lit (jliteral-long-dec-nouscores value)))
    (jliteralp lit))
  :rule-classes :rewrite)