Generate methods to convert to Java primitive arrays from lists.
(atj-gen-shallow-jprimarr-fromlist-methods fns) → methods
Function:
(defun atj-gen-shallow-jprimarr-fromlist-methods (fns) (declare (xargs :guard (symbol-listp fns))) (declare (xargs :guard (and (no-duplicatesp-eq fns) (subsetp-eq fns *atj-jprimarr-conv-fromlist-fns*)))) (let ((__function__ 'atj-gen-shallow-jprimarr-fromlist-methods)) (declare (ignorable __function__)) (cond ((endp fns) nil) (t (cons (atj-convert-expr-to-jprimarr-method (atj-jprimarr-conv-fromlist-fn-to-ptype (car fns))) (atj-gen-shallow-jprimarr-fromlist-methods (cdr fns)))))))
Theorem:
(defthm jmethod-listp-of-atj-gen-shallow-jprimarr-fromlist-methods (b* ((methods (atj-gen-shallow-jprimarr-fromlist-methods fns))) (jmethod-listp methods)) :rule-classes :rewrite)