coerce to a string
(String x) coerces x to a string.
The guard for string requires its argument to be a string, a
symbol, or a character.
- If x is already a string, then it is returned unchanged.
- If x is a symbol, then its symbol-name is returned.
- If x is a character, the corresponding one-character string is returned.
Note: this is a rather low-level operation that doesn't support coercing
numbers or conses into strings. If you want to turn numbers into strings, see
functions such as str::nat-to-dec-string, or more generally the str::numbers functions. For conses, see the str::pretty-printing
routines such as str::pretty.
String is a Common Lisp function. See any Common Lisp documentation
for more information.
(defun string (x)
(declare (xargs :guard (or (stringp x)
(cond ((stringp x) x)
((symbolp x) (symbol-name x))
(t (coerce (list x) 'string))))