► 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.4Characters

 procedure(alpha-char-p x) → t x : (characterp x)
Determines whether x is an alphabetic character.

Examples:

 > (alpha-char-p #\a) 't > (alpha-char-p #\3) '()

 procedure(char str n) → t str : (stringp str) n : (and (integerp n) (>= n 0) (< n (length str)))
Extracts the character at the nth (0-based) position in the string str.

Examples:

 > (char "hello" 0) #\h > (char "hello" 4) #\o

 procedure(char< x y) → t x : (characterp x) y : (characterp y)
Determines whether the character code of x is less than that of y.

Examples:

 > (char< #\a #\b) 't > (char< #\b #\a) '() > (char< #\b #\b) '() > (char< #\A #\a) 't

 procedure(char<= x y) → t x : (characterp x) y : (characterp y)
Determines whether the character code of x is less than or equal to that of y.

Examples:

 > (char<= #\a #\b) 't > (char<= #\b #\a) '() > (char<= #\b #\b) 't > (char<= #\A #\a) 't

 procedure(char> x y) → t x : (characterp x) y : (characterp y)
Determines whether the character code of x is greater than that of y.

Examples:

 > (char> #\a #\b) '() > (char> #\b #\a) 't > (char> #\b #\b) '() > (char> #\A #\a) '()

 procedure(char>= x y) → t x : (characterp x) y : (characterp y)
Determines whether the character code of x is greater than or equal to that of y.

Examples:

 > (char>= #\a #\b) '() > (char>= #\b #\a) 't > (char>= #\b #\b) 't > (char>= #\A #\a) '()

 procedure(char-code char) → t char : (characterp char)
Returns the numeric code for the given character.

Examples:

 > (char-code #\a) 97 > (char-code #\Z) 90

 procedure(char-downcase char) → t char : (and (characterp char) (standard-char-p str))
Converts the given character to lowercase

Examples:

 > (char-downcase #\A) #\a > (char-downcase #\a) #\a

 procedure(char-equal x y) → t x : (and (characterp x) (standard-char-p x)) y : (and (characterp y) (standard-char-p y))
Checks if the given characters are equal, ignoring to case.

Examples:

 > (char-equal #\a #\a) 't > (char-equal #\A #\a) 't

 procedure(char-upcase char) → t char : (and (characterp char) (standard-char-p str))
Converts the given character to uppercase

Examples:

 > (char-upcase #\A) #\A > (char-upcase #\a) #\A

 procedure(characterp x) → t x : t

Examples:

 > (characterp #\a) 't > (characterp "a") '()

 procedure(code-char x) → t x : (and (integerp x) (>= x 0) (< x 256))
Converts the given number into its character equivalent.

Examples:

 > (code-char 0) #\nul > (code-char 97) #\a > (code-char 255) #\ÿ > (code-char 1000) #\Ϩ

 procedure(digit-char-p x) → t x : (characterp x)
Determines whether the given character represents a numerical digit.

Examples:

 > (digit-char-p #\3) 3 > (digit-char-p #\a) '()

 procedure(digit-to-char n) → t n : (and (integerp n) (<= 0 n) (>= 15 n))
Converts the given number into its equivalent character in hex notation.

Examples:

 > (digit-to-char 7) #\7 > (digit-to-char 10) #\A > (digit-to-char 15) #\F

 procedure(lower-case-p x) → t x : (and (characterp x) (standard-char-p x))
Determines if x is a lowercase alphabetic character.

Examples:

 > (lower-case-p #\a) 't > (lower-case-p #\A) '()

 procedure(standard-char-p x) → t x : (characterp x)
Checks if the given character is a member of the *standard-chars*. This includes the standard punctuation and alphanumeric characters, along with #\newline and #\space.

Examples:

 > (standard-char-p #\a) 't > (standard-char-p #\5) 't > (standard-char-p #\tab) '()

 procedure(upper-case-p x) → t x : (and (characterp x) (standard-char-p x))
Determines if x is an upper-case alphabetic character.

Examples:

 > (upper-case-p #\A) 't > (upper-case-p #\a) '()