(vl-paramvaluelist-elim-useless-params current-place positions plainargs) → cleaned
Function:
(defun vl-paramvaluelist-elim-useless-params (current-place positions plainargs) (declare (xargs :guard (and (natp current-place) (integer-listp positions) (vl-paramvaluelist-p plainargs)))) (let ((__function__ 'vl-paramvaluelist-elim-useless-params)) (declare (ignorable __function__)) (cond ((atom plainargs) nil) ((member current-place positions) (vl-paramvaluelist-elim-useless-params (+ 1 current-place) positions (cdr plainargs))) (t (cons (car plainargs) (vl-paramvaluelist-elim-useless-params (+ 1 current-place) positions (cdr plainargs)))))))
Theorem:
(defthm vl-paramvaluelist-p-of-vl-paramvaluelist-elim-useless-params (implies (force (vl-paramvaluelist-p plainargs)) (b* ((cleaned (vl-paramvaluelist-elim-useless-params current-place positions plainargs))) (vl-paramvaluelist-p cleaned))) :rule-classes :rewrite)