(vl-package-lint-ignoreall x mashed-ignore-list) → new-x
Function:
(defun vl-package-lint-ignoreall (x mashed-ignore-list) (declare (xargs :guard (and (vl-package-p x) (string-listp mashed-ignore-list)))) (let ((__function__ 'vl-package-lint-ignoreall)) (declare (ignorable __function__)) (change-vl-package x :warnings (vl-warninglist-lint-ignoreall (vl-package->warnings x) mashed-ignore-list))))
Theorem:
(defthm vl-package-p-of-vl-package-lint-ignoreall (b* ((new-x (vl-package-lint-ignoreall x mashed-ignore-list))) (vl-package-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-package-lint-ignoreall-of-vl-package-fix-x (equal (vl-package-lint-ignoreall (vl-package-fix x) mashed-ignore-list) (vl-package-lint-ignoreall x mashed-ignore-list)))
Theorem:
(defthm vl-package-lint-ignoreall-vl-package-equiv-congruence-on-x (implies (vl-package-equiv x x-equiv) (equal (vl-package-lint-ignoreall x mashed-ignore-list) (vl-package-lint-ignoreall x-equiv mashed-ignore-list))) :rule-classes :congruence)
Theorem:
(defthm vl-package-lint-ignoreall-of-string-list-fix-mashed-ignore-list (equal (vl-package-lint-ignoreall x (string-list-fix mashed-ignore-list)) (vl-package-lint-ignoreall x mashed-ignore-list)))
Theorem:
(defthm vl-package-lint-ignoreall-string-list-equiv-congruence-on-mashed-ignore-list (implies (str::string-list-equiv mashed-ignore-list mashed-ignore-list-equiv) (equal (vl-package-lint-ignoreall x mashed-ignore-list) (vl-package-lint-ignoreall x mashed-ignore-list-equiv))) :rule-classes :congruence)