Change the location of some assignments.
(vl-relocate-assignments x loc) → new-x
Function:
(defun vl-relocate-assignments (x loc) (declare (xargs :guard (and (vl-assignlist-p x) (vl-location-p loc)))) (let ((__function__ 'vl-relocate-assignments)) (declare (ignorable __function__)) (if (atom x) nil (cons (change-vl-assign (car x) :loc loc) (vl-relocate-assignments (cdr x) loc)))))
Theorem:
(defthm vl-assignlist-p-of-vl-relocate-assignments (b* ((new-x (vl-relocate-assignments x loc))) (vl-assignlist-p new-x)) :rule-classes :rewrite)