Gather all top-level expressions from a vl-rangelist-p.
(vl-rangelist-allexprs x) → exprs
Function:
(defun vl-rangelist-allexprs (x) (declare (xargs :guard (vl-rangelist-p x))) (let ((__function__ 'vl-rangelist-allexprs)) (declare (ignorable __function__)) (mbe :logic (if (atom x) nil (append (vl-range-allexprs (car x)) (vl-rangelist-allexprs (cdr x)))) :exec (with-local-nrev (vl-rangelist-allexprs-nrev x nrev)))))
Theorem:
(defthm vl-exprlist-p-of-vl-rangelist-allexprs (b* ((exprs (vl-rangelist-allexprs x))) (vl-exprlist-p exprs)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-rangelist-allexprs (true-listp (vl-rangelist-allexprs x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-rangelist-allexprs-nrev-removal (equal (vl-rangelist-allexprs-nrev x nrev) (append nrev (vl-rangelist-allexprs x))))
Theorem:
(defthm set-equiv-congruence-over-vl-rangelist-allexprs (implies (set-equiv acl2::x acl2::y) (set-equiv (vl-rangelist-allexprs acl2::x) (vl-rangelist-allexprs acl2::y))) :rule-classes ((:congruence)))
Theorem:
(defthm subsetp-of-vl-rangelist-allexprs-when-subsetp (implies (subsetp acl2::x acl2::y) (subsetp (vl-rangelist-allexprs acl2::x) (vl-rangelist-allexprs acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm member-in-vl-rangelist-allexprs (implies (and (member acl2::k (vl-range-allexprs acl2::j)) (member acl2::j acl2::x)) (member acl2::k (vl-rangelist-allexprs acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-rangelist-allexprs-of-list-fix (equal (vl-rangelist-allexprs (list-fix acl2::x)) (vl-rangelist-allexprs acl2::x)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-rangelist-allexprs-of-append (equal (vl-rangelist-allexprs (append acl2::a acl2::b)) (append (vl-rangelist-allexprs acl2::a) (vl-rangelist-allexprs acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-rangelist-allexprs-when-not-consp (implies (not (consp acl2::x)) (equal (vl-rangelist-allexprs acl2::x) nil)) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-rangelist-allexprs-of-cons (equal (vl-rangelist-allexprs (cons acl2::a acl2::b)) (append (vl-range-allexprs acl2::a) (vl-rangelist-allexprs acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm vl-rangelist-allexprs-of-vl-rangelist-fix-x (equal (vl-rangelist-allexprs (vl-rangelist-fix x)) (vl-rangelist-allexprs x)))
Theorem:
(defthm vl-rangelist-allexprs-vl-rangelist-equiv-congruence-on-x (implies (vl-rangelist-equiv x x-equiv) (equal (vl-rangelist-allexprs x) (vl-rangelist-allexprs x-equiv))) :rule-classes :congruence)