		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-value-to-string-aux

Signature
(vl-value-to-string-aux value acc) → acc
Arguments: value — Guard (natp value).; acc — Guard (character-listp acc).
Returns: acc — Type (character-listp acc).

Definitions and Theorems

Function: vl-value-to-string-aux

(defun vl-value-to-string-aux (value acc)
  (declare (xargs :guard (and (natp value)
                              (character-listp acc))))
  (let ((__function__ 'vl-value-to-string-aux))
    (declare (ignorable __function__))
    (if (zp value)
        (character-list-fix acc)
      (vl-value-to-string-aux (ash (lnfix value) -8)
                              (cons (code-char (logand value 255))
                                    acc)))))

Theorem: character-listp-of-vl-value-to-string-aux

(defthm character-listp-of-vl-value-to-string-aux
  (b* ((acc (vl-value-to-string-aux value acc)))
    (character-listp acc))
  :rule-classes :rewrite)

Theorem: vl-value-to-string-aux-of-nfix-value

(defthm vl-value-to-string-aux-of-nfix-value
  (equal (vl-value-to-string-aux (nfix value)
                                 acc)
         (vl-value-to-string-aux value acc)))

Theorem: vl-value-to-string-aux-nat-equiv-congruence-on-value

(defthm vl-value-to-string-aux-nat-equiv-congruence-on-value
  (implies (acl2::nat-equiv value value-equiv)
           (equal (vl-value-to-string-aux value acc)
                  (vl-value-to-string-aux value-equiv acc)))
  :rule-classes :congruence)

Theorem: vl-value-to-string-aux-of-make-character-list-acc

(defthm vl-value-to-string-aux-of-make-character-list-acc
  (equal (vl-value-to-string-aux value (make-character-list acc))
         (vl-value-to-string-aux value acc)))

Theorem: vl-value-to-string-aux-charlisteqv-congruence-on-acc

(defthm vl-value-to-string-aux-charlisteqv-congruence-on-acc
  (implies (str::charlisteqv acc acc-equiv)
           (equal (vl-value-to-string-aux value acc)
                  (vl-value-to-string-aux value acc-equiv)))
  :rule-classes :congruence)