coerce to a string
The guard for
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.
(defun string (x) (declare (xargs :guard (or (stringp x) (symbolp x) (characterp x)))) (cond ((stringp x) x) ((symbolp x) (symbol-name x)) (t (coerce (list x) 'string))))