Major Section: ACL2-BUILT-INS
(String x) coerces x to a string. If x is already a
string, then it is returned unchanged; if x is a symbol, then its
symbol-name is returned; and if x is a character, the
corresponding one-character string is returned.
The guard for string requires its argument to be a string, a
symbol, or a character.
String is a Common Lisp function. See any Common Lisp
documentation for more information.
To see the ACL2 definition of this function, see pf.
