Explode a (resolved) vl2014::vl-hidexpr-p into a flat list of its components.
(vl2014::vl-explode-hid vl2014::x) → vl2014::pieces
Function:
(defun vl2014::vl-explode-hid (vl2014::x) (declare (xargs :guard (vl2014::vl-expr-p vl2014::x))) (declare (xargs :guard (and (vl2014::vl-hidexpr-p vl2014::x) (vl2014::vl-hidexpr-resolved-p vl2014::x)))) (let ((__function__ 'vl2014::vl-explode-hid)) (declare (ignorable __function__)) (if (vl2014::vl-hidexpr->endp vl2014::x) (list (vl2014::vl-hidname->name vl2014::x)) (append (vl2014::vl-explode-hidindex (vl2014::vl-hidexpr->first vl2014::x)) (vl2014::vl-explode-hid (vl2014::vl-hidexpr->rest vl2014::x))))))
Theorem:
(defthm vl2014::true-listp-of-vl-explode-hid (b* ((vl2014::pieces (vl2014::vl-explode-hid vl2014::x))) (true-listp vl2014::pieces)) :rule-classes :type-prescription)