Gather a flat list of all warnings from a vl-packagelist-p.
This is an ordinary defmapappend.
Function:
(defun vl-packagelist-flat-warnings (x) (declare (xargs :guard (vl-packagelist-p x))) (mbe :logic (if (consp x) (append (vl-package->warnings (car x)) (vl-packagelist-flat-warnings (cdr x))) nil) :exec (reverse (vl-packagelist-flat-warnings-exec x nil))))
Function:
(defun vl-packagelist-flat-warnings-exec (x acc) (declare (xargs :guard (vl-packagelist-p x))) (if (consp x) (vl-packagelist-flat-warnings-exec (cdr x) (revappend-without-guard (vl-package->warnings (car x)) acc)) acc))
Function:
(defun vl-packagelist-flat-warnings (x) (declare (xargs :guard (vl-packagelist-p x))) (mbe :logic (if (consp x) (append (vl-package->warnings (car x)) (vl-packagelist-flat-warnings (cdr x))) nil) :exec (reverse (vl-packagelist-flat-warnings-exec x nil))))
Theorem:
(defthm vl-packagelist-flat-warnings-exec-removal (equal (vl-packagelist-flat-warnings-exec acl2::x acl2::acc) (revappend (vl-packagelist-flat-warnings acl2::x) acl2::acc)) :rule-classes ((:rewrite)))
Theorem:
(defthm set-equiv-congruence-over-vl-packagelist-flat-warnings (implies (set-equiv acl2::x acl2::y) (set-equiv (vl-packagelist-flat-warnings acl2::x) (vl-packagelist-flat-warnings acl2::y))) :rule-classes ((:congruence)))
Theorem:
(defthm subsetp-of-vl-packagelist-flat-warnings-when-subsetp (implies (subsetp acl2::x acl2::y) (subsetp (vl-packagelist-flat-warnings acl2::x) (vl-packagelist-flat-warnings acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm member-in-vl-packagelist-flat-warnings (implies (and (member acl2::k (vl-package->warnings acl2::j)) (member acl2::j acl2::x)) (member acl2::k (vl-packagelist-flat-warnings acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-packagelist-flat-warnings-of-list-fix (equal (vl-packagelist-flat-warnings (list-fix acl2::x)) (vl-packagelist-flat-warnings acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-packagelist-flat-warnings-of-append (equal (vl-packagelist-flat-warnings (append acl2::a acl2::b)) (append (vl-packagelist-flat-warnings acl2::a) (vl-packagelist-flat-warnings acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-packagelist-flat-warnings-when-not-consp (implies (not (consp acl2::x)) (equal (vl-packagelist-flat-warnings acl2::x) nil)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-packagelist-flat-warnings-of-cons (equal (vl-packagelist-flat-warnings (cons acl2::a acl2::b)) (append (vl-package->warnings acl2::a) (vl-packagelist-flat-warnings acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-warninglist-p-of-vl-packagelist-flat-warnings (vl-warninglist-p (vl-packagelist-flat-warnings x)))