(s4vec-correct-formal-evals formals) → *
Function:
(defun s4vec-correct-formal-evals (formals) (declare (xargs :guard t)) (let ((__function__ 's4vec-correct-formal-evals)) (declare (ignorable __function__)) (if (atom formals) nil (cons (b* (((std::formal x1) (car formals))) (if (and (consp x1.guard) (eq (car x1.guard) 's4vec-p)) (cons 's4vec->4vec (cons x1.name 'nil)) x1.name)) (s4vec-correct-formal-evals (cdr formals))))))