Strings of ACL2 characters are written as sequences of characters delimited by ``double quotation marks'' ("). To put a double quotation mark in a string (or, any other character such as backslash or newline that seems to cause problems), 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