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