ACL2 Strings

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.

The function stringp recognizes strings and char 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 documentation.