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