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