► 1 ACL2
 ▼ 1.4 Functions and Macros
 1.4.1 Booleans 1.4.2 Symbols 1.4.3 Strings 1.4.4 Characters 1.4.5 Rational and Complex Arithmetic 1.4.6 Bitwise Operations 1.4.7 Ordinal Arithmetic 1.4.8 Lists 1.4.9 Association Lists 1.4.10 Sets 1.4.11 Trees 1.4.12 Sequences 1.4.13 IO
##### 1.4.3Strings

Some string functions can be found in the section on Sequences as well.

 (make-character-list x) → character-listp x : t
This function will coerce a value to a list of characters.
 Example: > (make-character-list "hello") ()

 (string x) → t x : (or (stringp x) (symbolp x) (characterp x))
Uses coerce to convert the input into a string.
 Examples: > (string "abc") "abc" > (string 'abc) "ABC" > (string #\a) "a"

 (string-append x y) → t x : (stringp x) y : (stringp y)
Concatenates two strings together.
 Example: > (string-append "ab" "cd") "abcd"

 (string-downcase str) → t str : (and (stringp str) (standard-char-listp (coerce str 'list)))
Converts the characters in str to lowercase.
 Example: > (string-downcase "ABCdef") "abcdef"

 (string-equal x y) → t x : (and (stringp x) (standard-char-listp (coerce x 'list))) y : (and (stringp y) (standard-char-listp (coerce y 'list)))
Compares two strings to see if they are equal.
 Examples: > (string-equal "ab" "cd") () > (string-equal "ab" "ab") t

 (string-upcase str) → t str : (and (stringp str) (standard-char-listp (coerce str 'list)))
Converts the characters in str to uppercase.
 Example: > (string-upcase "ABCdef") "ABCDEF"

 (string< x y) → t x : (stringp x) y : (stringp y)
Compares the two strings for lexicographical ordering. Returns non-nil if and only if x precedes y lexicographically. When non-nil, the number returned is the first position at which the strings differ.
 Examples: > (string< "ab" "cd") 0 > (string< "ab" "abc") 2

 (string<= x y) → t x : (stringp x) y : (stringp y)
Compares the two strings for lexicographical ordering. Returns non-nil if and only if x precedes y lexicographically. If they differ, the number returned is the first position at which the strings differ. Otherwise, the number returned is their common length.
 Examples: > (string<= "ab" "cd") 0 > (string<= "ab" "ab") 2

 (string> x y) → t x : (stringp x) y : (stringp y)
Compares the two strings for lexicographical ordering. Returns non-nil if and only if y precedes x lexicographically. When non-nil, the number returned is the first position at which the strings differ.
 Examples: > (string> "ab" "cd") () > (string> "ab" "ab") () > (string> "ba" "ab") 0

 (string>= x y) → t x : (stringp x) y : (stringp y)
Compares the two strings for lexicographical ordering. Returns non-nil if and only if y precedes x lexicographically. If they differ, the number returned is the first position at which the strings differ. Otherwise, the number returned is their common length.
 Examples: > (string>= "ab" "cd") () > (string>= "ab" "ab") 2 > (string>= "ba" "ab") 0

 (stringp x) → t x : t
Determines whether x is a string.
 Examples: > (stringp "abcd") t > (stringp nil) ()