ACL2 Strings
ACL2 Strings
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 (\).
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.
