		Search-engine friendly clone of the ACL2 documentation.

Sv::vl-expr.lisp

Vl-integer-to-string

Signature
(vl-integer-to-string val) → *
Arguments: val — Guard (vl-value-p val).

Definitions and Theorems

Function: vl-integer-to-string

(defun vl-integer-to-string (val)
  (declare (xargs :guard (vl-value-p val)))
  (declare (xargs :guard (vl-value-case val :vl-constint)))
  (let ((__function__ 'vl-integer-to-string))
    (declare (ignorable __function__))
    (implode (vl-value-to-string-aux (vl-constint->value val)
                                     nil))))

Theorem: vl-integer-to-string-of-vl-value-fix-val

(defthm vl-integer-to-string-of-vl-value-fix-val
  (equal (vl-integer-to-string (vl-value-fix val))
         (vl-integer-to-string val)))

Theorem: vl-integer-to-string-vl-value-equiv-congruence-on-val

(defthm vl-integer-to-string-vl-value-equiv-congruence-on-val
  (implies (vl-value-equiv val val-equiv)
           (equal (vl-integer-to-string val)
                  (vl-integer-to-string val-equiv)))
  :rule-classes :congruence)