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