		Search-engine friendly clone of the ACL2 documentation.

Extended-characters

Vl-echarlist->string

Transform a vl-echarlist-p to a string.

Signature
(vl-echarlist->string x) → *
Arguments: x — Guard (vl-echarlist-p x).

Logically, this function just runs vl-echarlist->chars and coerces the result to a string; we typically leave it enabled.

Under the hood, in Common Lisp, we install a faster definition that avoids creating an intermediate list and instead just builds a string directly. This notably saves a lot of memory when we build vl-filemap-ps.

Definitions and Theorems

Function: vl-echarlist->string

(defun vl-echarlist->string (x)
  (declare (xargs :guard (vl-echarlist-p x)))
  (let ((__function__ 'vl-echarlist->string))
    (declare (ignorable __function__))
    (implode (vl-echarlist->chars x))))

Theorem: vl-echarlist->string-of-vl-echarlist-fix-x

(defthm vl-echarlist->string-of-vl-echarlist-fix-x
  (equal (vl-echarlist->string (vl-echarlist-fix x))
         (vl-echarlist->string x)))

Theorem: vl-echarlist->string-vl-echarlist-equiv-congruence-on-x

(defthm vl-echarlist->string-vl-echarlist-equiv-congruence-on-x
  (implies (vl-echarlist-equiv x x-equiv)
           (equal (vl-echarlist->string x)
                  (vl-echarlist->string x-equiv)))
  :rule-classes :congruence)