(vl-collect-original-elements-matching-dupe dupe fixed orig) → matches
Function:
(defun vl-collect-original-elements-matching-dupe (dupe fixed orig) (declare (xargs :guard (and (vl-modelement-p dupe) (vl-modelementlist-p fixed) (vl-modelementlist-p orig)))) (declare (xargs :guard (same-lengthp fixed orig))) (let ((__function__ 'vl-collect-original-elements-matching-dupe)) (declare (ignorable __function__)) (b* (((when (atom fixed)) nil) (rest (vl-collect-original-elements-matching-dupe dupe (cdr fixed) (cdr orig))) ((when (equal dupe (car fixed))) (cons (vl-modelement-fix (car orig)) rest))) rest)))
Theorem:
(defthm vl-modelementlist-p-of-vl-collect-original-elements-matching-dupe (b* ((matches (vl-collect-original-elements-matching-dupe dupe fixed orig))) (vl-modelementlist-p matches)) :rule-classes :rewrite)