Recognizer the ACL2 function symbols that model the conversions to Java primitive arrays from ACL2 lists.
(atj-jprimarr-conv-fromlist-fn-p fn) → yes/no
Function:
(defun atj-jprimarr-conv-fromlist-fn-p (fn) (declare (xargs :guard t)) (let ((__function__ 'atj-jprimarr-conv-fromlist-fn-p)) (declare (ignorable __function__)) (and (member-eq fn *atj-jprimarr-conv-fromlist-fns*) t)))
Theorem:
(defthm booleanp-of-atj-jprimarr-conv-fromlist-fn-p (b* ((yes/no (atj-jprimarr-conv-fromlist-fn-p fn))) (booleanp yes/no)) :rule-classes :rewrite)