(vl-remove-fake-function-vardecls x) → new-x
Function:
(defun vl-remove-fake-function-vardecls (x) (declare (xargs :guard (vl-vardecllist-p x))) (let ((__function__ 'vl-remove-fake-function-vardecls)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) (x1 (vl-vardecl-fix (car x))) ((when (assoc-equal "VL_HIDDEN_DECL_FOR_TASKPORT" (vl-vardecl->atts x1))) (vl-remove-fake-function-vardecls (cdr x)))) (cons x1 (vl-remove-fake-function-vardecls (cdr x))))))
Theorem:
(defthm vl-vardecllist-p-of-vl-remove-fake-function-vardecls (b* ((new-x (vl-remove-fake-function-vardecls x))) (vl-vardecllist-p new-x)) :rule-classes :rewrite)