Strings of ACL2 characters are written as sequences of characters delimited by ``double quotation marks'' ("). To put such a character in a string, escape it by preceding it with a backslash.
stringp recognizes strings and
will fetch the nth character of a string. There are many
other primitives for handling strings, such as
comparing two strings lexicographically. We suggest you
See programming where we list all of the primitive ACL2
functions. Alternatively, see any Common Lisp language