		Search-engine friendly clone of the ACL2 documentation.

Programming

Strings

Strings are atomic objects that contain character sequences, like "Hello World".

See the std/strings library for many additional string functions and lemmas about the built-in string functions.

Subtopics

Std/strings: A library with many useful functions for working with strings, and for reasoning about ACL2's built-in string operations and these new operations.
String-listp: Recognizer for a true list of strings
Stringp: Recognizer for strings
Length: Length of a string or proper list
Search: Search for a string or list in another string or list
Remove-duplicates: Remove duplicates from a string or a list
Position: Position of an item in a string or a list
Coerce: Coerce a character list to a string and a string to a list
Concatenate: Concatenate lists or strings together
Reverse: Reverse a list or string
String: coerce to a string
Subseq: Subsequence of a string or list
Substitute: Substitute into a string or a list, using eql as test
String-upcase: In a given string, turn lower-case characters into upper-case
String-downcase: In a given string, turn upper-case characters into lower-case
Count: Count the number of occurrences of an item in a string or true-list
Char: The nth element (zero-based) of a string
String<: Less-than test for strings
String-equal: String equality without regard to case
String-utilities: Some utilities for strings (and characters).
String-append: concatenate two strings
String>=: Less-than-or-equal test for strings
String<=: Less-than-or-equal test for strings
String>: Greater-than test for strings
Hex-digit-char-theorems: Some theorems about the library functions str::hex-digit-char-value and str::hex-digit-to-char.
String-downcase-gen: Downcase any string (even ones with non-standard characters).
String-upcase-gen: Upcase any string (even ones with non-standard characters).