		Search-engine friendly clone of the ACL2 documentation.

Vl-flatten-hidindex

Vl-flatten-hidindex-aux

Signature
(vl-flatten-hidindex-aux indices acc) → new-acc
Arguments: indices — Guard (and (vl-exprlist-p indices) (vl-exprlist-resolved-p indices)).
Returns: new-acc — Type (character-listp new-acc), given (character-listp acc).

Definitions and Theorems

Function: vl-flatten-hidindex-aux

(defun vl-flatten-hidindex-aux (indices acc)
 (declare (xargs :guard (and (vl-exprlist-p indices)
                             (vl-exprlist-resolved-p indices))))
 (let ((__function__ 'vl-flatten-hidindex-aux))
  (declare (ignorable __function__))
  (b*
   (((when (atom indices)) acc)
    (acc (cons #\[ acc))
    (acc
       (revappend
            (str::nat-to-dec-chars (vl-resolved->val (car indices)))
            acc))
    (acc (cons #\] acc)))
   (vl-flatten-hidindex-aux (cdr indices)
                            acc))))

Theorem: character-listp-of-vl-flatten-hidindex-aux

(defthm character-listp-of-vl-flatten-hidindex-aux
  (implies (character-listp acc)
           (b* ((new-acc (vl-flatten-hidindex-aux indices acc)))
             (character-listp new-acc)))
  :rule-classes :rewrite)