		Search-engine friendly clone of the ACL2 documentation.

Implode

Convert a character list into a string.

Signature
(implode x) → str
Arguments: x — Guard (character-listp x).
Returns: str — Type (stringp str).

(implode x) is logically nothing more than (coerce x 'string).

Even though coerce is built into ACL2, we prefer to use implode as our normal form. We rewrite all uses of (coerce x 'string) into (str::implode x) with the following rule:

Theorem: coerce-to-string-removal

(defthm coerce-to-string-removal
  (equal (coerce x 'string) (implode x)))

The basic rationale for this is that coerce's extra 'string argument means we can't write, e.g., congruence relations about (coerce x 'string), whereas this is no problem for (implode x).

We do the same thing for (coerce x 'list) — see explode.

Definitions and Theorems

Function: implode$inline

(defun acl2::implode$inline (x)
  (declare (xargs :guard (character-listp x)))
  (let ((acl2::__function__ 'implode))
    (declare (ignorable acl2::__function__))
    (coerce x 'string)))

Theorem: stringp-of-implode

(defthm acl2::stringp-of-implode
  (b* ((str (acl2::implode$inline x)))
    (stringp str))
  :rule-classes :type-prescription)

Theorem: equal-of-implodes

(defthm equal-of-implodes
  (implies (and (character-listp x)
                (character-listp y))
           (equal (equal (implode x) (implode y))
                  (equal x y))))

Theorem: implode-of-make-character-list

(defthm implode-of-make-character-list
  (equal (implode (make-character-list x))
         (implode x)))

Theorem: equal-of-implode-with-empty-string

(defthm equal-of-implode-with-empty-string
  (equal (equal "" (implode x)) (atom x)))

Theorem: coerce-to-string-removal

(defthm coerce-to-string-removal
  (equal (coerce x 'string) (implode x)))

Subtopics

Explode-implode-equalities: Theorems about equalities involving explode and implode.
Implode-explode-inversion: Inversion theorems for implode and explode.