Lift jparam->type to lists.
(jparam-list->types params) → types
Function:
(defun jparam-list->types (params) (declare (xargs :guard (jparam-listp params))) (let ((__function__ 'jparam-list->types)) (declare (ignorable __function__)) (cond ((endp params) nil) (t (cons (jparam->type (car params)) (jparam-list->types (cdr params)))))))
Theorem:
(defthm jtype-listp-of-jparam-list->types (b* ((types (jparam-list->types params))) (jtype-listp types)) :rule-classes :rewrite)
Theorem:
(defthm len-of-jparam-list->types (equal (len (jparam-list->types params)) (len params)) :rule-classes :linear)