Build a Java expression consisting of
a
Function:
(defun jexpr-lit-long-dec-nouscores (value) (declare (xargs :guard (natp value))) (let ((__function__ 'jexpr-lit-long-dec-nouscores)) (declare (ignorable __function__)) (jexpr-literal (jliteral-long-dec-nouscores value))))
Theorem:
(defthm jexprp-of-jexpr-lit-long-dec-nouscores (b* ((expr (jexpr-lit-long-dec-nouscores value))) (jexprp expr)) :rule-classes :rewrite)