(vl-namedparamvaluelist-elim-useless-params names namedargs) → cleaned
Function:
(defun vl-namedparamvaluelist-elim-useless-params (names namedargs) (declare (xargs :guard (and (string-listp names) (vl-namedparamvaluelist-p namedargs)))) (let ((__function__ 'vl-namedparamvaluelist-elim-useless-params)) (declare (ignorable __function__)) (cond ((atom namedargs) nil) ((member-equal (vl-namedparamvalue->name (car namedargs)) names) (vl-namedparamvaluelist-elim-useless-params names (cdr namedargs))) (t (cons (car namedargs) (vl-namedparamvaluelist-elim-useless-params names (cdr namedargs)))))))
Theorem:
(defthm vl-namedparamvaluelist-p-of-vl-namedparamvaluelist-elim-useless-params (implies (force (vl-namedparamvaluelist-p namedargs)) (b* ((cleaned (vl-namedparamvaluelist-elim-useless-params names namedargs))) (vl-namedparamvaluelist-p cleaned))) :rule-classes :rewrite)