(vl-flatten-hidindex-aux indices acc) → new-acc
Function:
(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:
(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)