Build a Java
This is an integer decimal literal without the type suffix.
Function:
(defun jliteral-int-dec-nouscores (value) (declare (xargs :guard (natp value))) (let ((__function__ 'jliteral-int-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-none)))))))
Theorem:
(defthm jliteralp-of-jliteral-int-dec-nouscores (b* ((lit (jliteral-int-dec-nouscores value))) (jliteralp lit)) :rule-classes :rewrite)