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
string< for comparing two strings
lexicographically. We suggest you See programming where we list all
of the primitive ACL2 functions. Alternatively, see any Common Lisp language