Recognize the ACL2 function symbols that model the Java primitive value constructions, operations, and conversions.
(atj-jprim-fn-p fn) → yes/no
Function:
(defun atj-jprim-fn-p (fn) (declare (xargs :guard t)) (let ((__function__ 'atj-jprim-fn-p)) (declare (ignorable __function__)) (and (member-eq fn *atj-jprim-fns*) t)))
Theorem:
(defthm booleanp-of-atj-jprim-fn-p (b* ((yes/no (atj-jprim-fn-p fn))) (booleanp yes/no)) :rule-classes :rewrite)