Lift fresh-namep-msg-weak to lists.
(fresh-name-listp-msg-weak names type wrld) → msg/nil
As soon as one name in the list fails the test, stop and return the message.
If all the names are fresh, return
Function:
(defun fresh-name-listp-msg-weak (names type wrld) (declare (xargs :guard (and (symbol-listp names) (plist-worldp wrld)))) (declare (xargs :guard (member-eq type '(function macro const stobj constrained-function nil)))) (let ((__function__ 'fresh-name-listp-msg-weak)) (declare (ignorable __function__)) (cond ((endp names) nil) (t (or (fresh-namep-msg-weak (car names) type wrld) (fresh-name-listp-msg-weak (cdr names) type wrld))))))