(vl-interfacelist-suppress-file-warnings x suppress-files) maps vl-interface-suppress-file-warnings across a list.
(vl-interfacelist-suppress-file-warnings x suppress-files) → new-x
This is an ordinary defprojection.
Function:
(defun vl-interfacelist-suppress-file-warnings-exec (x suppress-files acc) (declare (xargs :guard (and (vl-interfacelist-p x) (string-listp suppress-files)))) (declare (xargs :guard t)) (let ((__function__ 'vl-interfacelist-suppress-file-warnings-exec)) (declare (ignorable __function__)) (if (consp x) (vl-interfacelist-suppress-file-warnings-exec (cdr x) suppress-files (cons (vl-interface-suppress-file-warnings (car x) suppress-files) acc)) acc)))
Function:
(defun vl-interfacelist-suppress-file-warnings-nrev (x suppress-files nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (and (vl-interfacelist-p x) (string-listp suppress-files)))) (declare (xargs :guard t)) (let ((__function__ 'vl-interfacelist-suppress-file-warnings-nrev)) (declare (ignorable __function__)) (if (atom x) (nrev-fix nrev) (let ((nrev (nrev-push (vl-interface-suppress-file-warnings (car x) suppress-files) nrev))) (vl-interfacelist-suppress-file-warnings-nrev (cdr x) suppress-files nrev)))))
Function:
(defun vl-interfacelist-suppress-file-warnings (x suppress-files) (declare (xargs :guard (and (vl-interfacelist-p x) (string-listp suppress-files)))) (declare (xargs :guard t)) (let ((__function__ 'vl-interfacelist-suppress-file-warnings)) (declare (ignorable __function__)) (mbe :logic (if (consp x) (cons (vl-interface-suppress-file-warnings (car x) suppress-files) (vl-interfacelist-suppress-file-warnings (cdr x) suppress-files)) nil) :exec (if (atom x) nil (with-local-nrev (vl-interfacelist-suppress-file-warnings-nrev x suppress-files nrev))))))
Theorem:
(defthm vl-interfacelist-p-of-vl-interfacelist-suppress-file-warnings (b* ((new-x (vl-interfacelist-suppress-file-warnings x suppress-files))) (vl-interfacelist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-vl-interfacelist-fix-x (equal (vl-interfacelist-suppress-file-warnings (vl-interfacelist-fix x) suppress-files) (vl-interfacelist-suppress-file-warnings x suppress-files)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-vl-interfacelist-equiv-congruence-on-x (implies (vl-interfacelist-equiv x x-equiv) (equal (vl-interfacelist-suppress-file-warnings x suppress-files) (vl-interfacelist-suppress-file-warnings x-equiv suppress-files))) :rule-classes :congruence)
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-string-list-fix-suppress-files (equal (vl-interfacelist-suppress-file-warnings x (string-list-fix suppress-files)) (vl-interfacelist-suppress-file-warnings x suppress-files)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-string-list-equiv-congruence-on-suppress-files (implies (str::string-list-equiv suppress-files suppress-files-equiv) (equal (vl-interfacelist-suppress-file-warnings x suppress-files) (vl-interfacelist-suppress-file-warnings x suppress-files-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-update-nth (implies (<= (nfix acl2::n) (len acl2::x)) (equal (vl-interfacelist-suppress-file-warnings (update-nth acl2::n acl2::v acl2::x) suppress-files) (update-nth acl2::n (vl-interface-suppress-file-warnings acl2::v suppress-files) (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-revappend (equal (vl-interfacelist-suppress-file-warnings (revappend acl2::x acl2::y) suppress-files) (revappend (vl-interfacelist-suppress-file-warnings acl2::x suppress-files) (vl-interfacelist-suppress-file-warnings acl2::y suppress-files))) :rule-classes ((:rewrite)))
Theorem:
(defthm nthcdr-of-vl-interfacelist-suppress-file-warnings (equal (nthcdr acl2::n (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)) (vl-interfacelist-suppress-file-warnings (nthcdr acl2::n acl2::x) suppress-files)) :rule-classes ((:rewrite)))
Theorem:
(defthm nth-of-vl-interfacelist-suppress-file-warnings (equal (nth acl2::n (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)) (and (< (nfix acl2::n) (len acl2::x)) (vl-interface-suppress-file-warnings (nth acl2::n acl2::x) suppress-files))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-take (implies (<= (nfix acl2::n) (len acl2::x)) (equal (vl-interfacelist-suppress-file-warnings (take acl2::n acl2::x) suppress-files) (take acl2::n (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)))) :rule-classes ((:rewrite)))
Theorem:
(defthm set-equiv-congruence-over-vl-interfacelist-suppress-file-warnings (implies (set-equiv acl2::x acl2::y) (set-equiv (vl-interfacelist-suppress-file-warnings acl2::x suppress-files) (vl-interfacelist-suppress-file-warnings acl2::y suppress-files))) :rule-classes ((:congruence)))
Theorem:
(defthm subsetp-of-vl-interfacelist-suppress-file-warnings-when-subsetp (implies (subsetp acl2::x acl2::y) (subsetp (vl-interfacelist-suppress-file-warnings acl2::x suppress-files) (vl-interfacelist-suppress-file-warnings acl2::y suppress-files))) :rule-classes ((:rewrite)))
Theorem:
(defthm member-of-vl-interface-suppress-file-warnings-in-vl-interfacelist-suppress-file-warnings (implies (member acl2::k acl2::x) (member (vl-interface-suppress-file-warnings acl2::k suppress-files) (vl-interfacelist-suppress-file-warnings acl2::x suppress-files))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-nrev-removal (equal (vl-interfacelist-suppress-file-warnings-nrev acl2::x suppress-files nrev) (append nrev (vl-interfacelist-suppress-file-warnings acl2::x suppress-files))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-exec-removal (equal (vl-interfacelist-suppress-file-warnings-exec acl2::x suppress-files acl2::acc) (revappend (vl-interfacelist-suppress-file-warnings acl2::x suppress-files) acl2::acc)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-rev (equal (vl-interfacelist-suppress-file-warnings (rev acl2::x) suppress-files) (rev (vl-interfacelist-suppress-file-warnings acl2::x suppress-files))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-list-fix (equal (vl-interfacelist-suppress-file-warnings (list-fix acl2::x) suppress-files) (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-append (equal (vl-interfacelist-suppress-file-warnings (append acl2::a acl2::b) suppress-files) (append (vl-interfacelist-suppress-file-warnings acl2::a suppress-files) (vl-interfacelist-suppress-file-warnings acl2::b suppress-files))) :rule-classes ((:rewrite)))
Theorem:
(defthm cdr-of-vl-interfacelist-suppress-file-warnings (equal (cdr (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)) (vl-interfacelist-suppress-file-warnings (cdr acl2::x) suppress-files)) :rule-classes ((:rewrite)))
Theorem:
(defthm car-of-vl-interfacelist-suppress-file-warnings (equal (car (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)) (and (consp acl2::x) (vl-interface-suppress-file-warnings (car acl2::x) suppress-files))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-under-iff (iff (vl-interfacelist-suppress-file-warnings acl2::x suppress-files) (consp acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm consp-of-vl-interfacelist-suppress-file-warnings (equal (consp (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)) (consp acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm len-of-vl-interfacelist-suppress-file-warnings (equal (len (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)) (len acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-of-vl-interfacelist-suppress-file-warnings (true-listp (vl-interfacelist-suppress-file-warnings acl2::x suppress-files)) :rule-classes :type-prescription)
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-when-not-consp (implies (not (consp acl2::x)) (equal (vl-interfacelist-suppress-file-warnings acl2::x suppress-files) nil)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-interfacelist-suppress-file-warnings-of-cons (equal (vl-interfacelist-suppress-file-warnings (cons acl2::a acl2::b) suppress-files) (cons (vl-interface-suppress-file-warnings acl2::a suppress-files) (vl-interfacelist-suppress-file-warnings acl2::b suppress-files))) :rule-classes ((:rewrite)))