Assign DIR to every argument in the list X.
(vl-plainarglist-assign-dir dir x) → new-x
Function:
(defun vl-plainarglist-assign-dir (dir x) (declare (xargs :guard (and (vl-direction-p dir) (vl-plainarglist-p x)))) (let ((__function__ 'vl-plainarglist-assign-dir)) (declare (ignorable __function__)) (if (atom x) nil (cons (change-vl-plainarg (car x) :dir (vl-direction-fix dir)) (vl-plainarglist-assign-dir dir (cdr x))))))
Theorem:
(defthm vl-plainarglist-p-of-vl-plainarglist-assign-dir (b* ((new-x (vl-plainarglist-assign-dir dir x))) (vl-plainarglist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-plainarglist-assign-dir-of-vl-direction-fix-dir (equal (vl-plainarglist-assign-dir (vl-direction-fix dir) x) (vl-plainarglist-assign-dir dir x)))
Theorem:
(defthm vl-plainarglist-assign-dir-vl-direction-equiv-congruence-on-dir (implies (vl-direction-equiv dir dir-equiv) (equal (vl-plainarglist-assign-dir dir x) (vl-plainarglist-assign-dir dir-equiv x))) :rule-classes :congruence)
Theorem:
(defthm vl-plainarglist-assign-dir-of-vl-plainarglist-fix-x (equal (vl-plainarglist-assign-dir dir (vl-plainarglist-fix x)) (vl-plainarglist-assign-dir dir x)))
Theorem:
(defthm vl-plainarglist-assign-dir-vl-plainarglist-equiv-congruence-on-x (implies (vl-plainarglist-equiv x x-equiv) (equal (vl-plainarglist-assign-dir dir x) (vl-plainarglist-assign-dir dir x-equiv))) :rule-classes :congruence)