		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 (vl-exprlist-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 (vl-exprlist-p indices)))
  (declare (xargs :guard (vl-exprlist-resolved-p indices)))
  (let ((__function__ 'vl-flatten-hidindex-aux))
    (declare (ignorable __function__))
    (b* (((when (atom indices)) acc)
         (acc (cons #\[ acc))
         (idx (vl-resolved->val (car indices)))
         (acc (if (< idx 0) (cons #\- acc) acc))
         (acc (revappend (str::nat-to-dec-chars (abs idx))
                         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)

Theorem: vl-flatten-hidindex-aux-of-vl-exprlist-fix-indices

(defthm vl-flatten-hidindex-aux-of-vl-exprlist-fix-indices
  (equal (vl-flatten-hidindex-aux (vl-exprlist-fix indices)
                                  acc)
         (vl-flatten-hidindex-aux indices acc)))

Theorem: vl-flatten-hidindex-aux-vl-exprlist-equiv-congruence-on-indices

(defthm
    vl-flatten-hidindex-aux-vl-exprlist-equiv-congruence-on-indices
  (implies (vl-exprlist-equiv indices indices-equiv)
           (equal (vl-flatten-hidindex-aux indices acc)
                  (vl-flatten-hidindex-aux indices-equiv acc)))
  :rule-classes :congruence)