Coerce
Coerce a character list to a string and a string to a list
Completion Axiom (completion-of-coerce):
(equal (coerce x y)
(cond
((equal y 'list)
(if (stringp x)
(coerce x 'list)
nil))
(t
(coerce (make-character-list x) 'string))))
Guard for (coerce x y):
(if (equal y 'list)
(stringp x)
(if (equal y 'string)
(character-listp x)
nil))
Also see community book books/misc/fast-coerce.lisp, contributed by
Jared Davis, for a version of coerce that may be faster for Common Lisp
implementations other than CCL 1.3 or later, if the second argument is
'list (for coercing a string to a list).
Logical Note
The function coerce can be viewed as the constructor for strings. As
discussed in Section 7 of "A Precise
Description of the ACL2 Logic" (Matt Kaufmann and J Moore, April, 1998),
a string may be built by coercing its list of characters: for example,
"abc" is (coerce '(#\a #\b #\c) 'string). More precisely,
"abc" is an abbreviation for (coerce '(#\a #\b #\c) 'string),
where even more pedantically, '(#\a #\b #\c) is an abbreviation for
(cons '#\a (cons '#\b (cons '#\c 'nil))).
Subtopics
- Explode
- Convert a string to a character list.
- Implode
- Convert a character list into a string.
- Std/strings/coerce
- Lemmas about coerce available in the std/strings library.
