(identifier-list-names ids) → l
Function:
(defun identifier-list-names (ids) (declare (xargs :guard (identifier-listp ids))) (let ((__function__ 'identifier-list-names)) (declare (ignorable __function__)) (if (endp ids) nil (cons (identifier->name (car ids)) (identifier-list-names (cdr ids))))))
Theorem:
(defthm string-listp-of-identifier-list-names (b* ((l (identifier-list-names ids))) (string-listp l)) :rule-classes :rewrite)