Generate a Java formal parameter list from the specified names and Java types.
(atj-gen-paramlist names types) → params
Given a list of Java parameter names and a list of Java types, this function generates a Java formal parameter list that associates each type to each name, in order.
Function:
(defun atj-gen-paramlist (names types) (declare (xargs :guard (and (string-listp names) (jtype-listp types)))) (declare (xargs :guard (= (len names) (len types)))) (let ((__function__ 'atj-gen-paramlist)) (declare (ignorable __function__)) (cond ((endp names) nil) (t (cons (make-jparam :final? nil :type (car types) :name (car names)) (atj-gen-paramlist (cdr names) (cdr types)))))))
Theorem:
(defthm jparam-listp-of-atj-gen-paramlist (b* ((params (atj-gen-paramlist names types))) (jparam-listp params)) :rule-classes :rewrite)