		Search-engine friendly clone of the ACL2 documentation.

Stv-hid-parse

Vl2014::vl-explode-hidindex

Explode a (resolved) vl2014::vl-hidindex-p into a flat list of its components.

Signature
(vl2014::vl-explode-hidindex vl2014::x) → vl2014::pieces
Arguments: vl2014::x — The hidindex to explode, e.g., foo[3][4][5].
Guard (vl2014::vl-expr-p vl2014::x).
Returns: vl2014::pieces — A flat, mixed list of strings and numbers, e.g., ("foo" 3 4 5).
Type (true-listp vl2014::pieces).

Definitions and Theorems

Function: vl-explode-hidindex

(defun vl2014::vl-explode-hidindex (vl2014::x)
 (declare (xargs :guard (vl2014::vl-expr-p vl2014::x)))
 (declare
    (xargs :guard (and (vl2014::vl-hidindex-p vl2014::x)
                       (vl2014::vl-hidindex-resolved-p vl2014::x))))
 (let ((__function__ 'vl2014::vl-explode-hidindex))
   (declare (ignorable __function__))
   (b* ((vl2014::name (vl2014::vl-hidindex->name vl2014::x))
        (vl2014::indices (vl2014::vl-hidindex->indices vl2014::x)))
     (cons vl2014::name
           (vl2014::vl-exprlist-resolved->vals vl2014::indices)))))

Theorem: true-listp-of-vl-explode-hidindex

(defthm vl2014::true-listp-of-vl-explode-hidindex
  (b* ((vl2014::pieces (vl2014::vl-explode-hidindex vl2014::x)))
    (true-listp vl2014::pieces))
  :rule-classes :type-prescription)