Convert each plainarglist in a vl-plainarglistlist-p into an vl-arguments-p.
(vl-plainarglists-to-arguments x) → args
Function:
(defun vl-plainarglists-to-arguments (x) (declare (xargs :guard (vl-plainarglistlist-p x))) (let ((__function__ 'vl-plainarglists-to-arguments)) (declare (ignorable __function__)) (if (consp x) (cons (make-vl-arguments-plain :args (car x)) (vl-plainarglists-to-arguments (cdr x))) nil)))
Theorem:
(defthm vl-argumentlist-p-of-vl-plainarglists-to-arguments (b* ((args (vl-plainarglists-to-arguments x))) (vl-argumentlist-p args)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-plainarglists-to-arguments (equal (len (vl-plainarglists-to-arguments x)) (len x)))
Theorem:
(defthm vl-plainarglists-to-arguments-of-vl-plainarglistlist-fix-x (equal (vl-plainarglists-to-arguments (vl-plainarglistlist-fix x)) (vl-plainarglists-to-arguments x)))
Theorem:
(defthm vl-plainarglists-to-arguments-vl-plainarglistlist-equiv-congruence-on-x (implies (vl-plainarglistlist-equiv x x-equiv) (equal (vl-plainarglists-to-arguments x) (vl-plainarglists-to-arguments x-equiv))) :rule-classes :congruence)