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