(vl-strip-locs-from-importresult-alist x) → new-x
Function:
(defun vl-strip-locs-from-importresult-alist (x) (declare (xargs :guard (vl-importresult-alist-p x))) (let ((__function__ 'vl-strip-locs-from-importresult-alist)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((cons key val) (car x))) (cons (cons (string-fix key) (change-vl-importresult val :loc *vl-fakeloc*)) (vl-strip-locs-from-importresult-alist (cdr x))))))
Theorem:
(defthm vl-importresult-alist-p-of-vl-strip-locs-from-importresult-alist (b* ((new-x (vl-strip-locs-from-importresult-alist x))) (vl-importresult-alist-p new-x)) :rule-classes :rewrite)