Convert a string to a character list.

- Signature
(explode x) → chars

- Returns
`chars`—Type (character-listp chars) .

`(explode x)` is logically nothing more than

Even though coerce is built into ACL2, we prefer to use

**Theorem: **

(defthm coerce-to-list-removal (equal (coerce x 'list) (explode x)))

The basic rationale for this is that

We do the same thing for

**BOZO** consider using misc/fast-coerce here.

**Function: **

(defun acl2::explode$inline (x) (declare (type string x)) (let ((acl2::__function__ 'explode)) (declare (ignorable acl2::__function__)) (coerce x 'list)))

**Theorem: **

(defthm acl2::character-listp-of-explode (b* ((chars (acl2::explode$inline x))) (character-listp chars)) :rule-classes :rewrite)

**Theorem: **

(defthm true-listp-of-explode (true-listp (explode x)) :rule-classes :type-prescription)

**Theorem: **

(defthm explode-when-not-stringp (implies (not (stringp x)) (equal (explode x) nil)))

**Theorem: **

(defthm equal-of-explodes (implies (and (stringp x) (stringp y)) (equal (equal (explode x) (explode y)) (equal x y))))

**Theorem: **

(defthm explode-under-iff (iff (explode string) (and (stringp string) (not (equal "" string)))))

**Theorem: **

(defthm consp-of-explode (equal (consp (explode string)) (and (stringp string) (not (equal "" string)))))

**Theorem: **

(defthm coerce-to-list-removal (equal (coerce x 'list) (explode x)))

- Implode-explode-inversion
- Inversion theorems for implode and explode.