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.