		Search-engine friendly clone of the ACL2 documentation.

String

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.

Function: string

(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))))