Is the character in the string?

>>> :set -XOverloadedStrings
>>> prove $ \c -> c `elem` singleton c
Q.E.D.
>>> prove $ \c -> bnot (c `elem` "")
Q.E.D.

Is the character not in the string?

>>> prove $ \c s -> c `elem` s <=> bnot (c `notElem` s)
Q.E.D.

The ord of a character.

Conversion from an integer to a character.

>>> prove $ \x -> 0 .<= x &&& x .< 256 ==> ord (chr x) .== x
Q.E.D.
>>> prove $ \x -> chr (ord x) .== x
Q.E.D.

Convert to lower-case.

>>> prove $ \c -> toLower (toLower c) .== toLower c
Q.E.D.
>>> prove $ \c -> isLower c ==> toLower (toUpper c) .== c
Q.E.D.

Convert to upper-case. N.B. There are three special cases!

• The character 223 is special. It corresponds to the German Eszett, it is considered lower-case, and furthermore it's upper-case maps back to itself within our character-set. So, we leave it untouched.
• The character 181 maps to upper-case 924, which is beyond our character set. We leave it untouched. (This is the A with an acute accent.)
• The character 255 maps to upper-case 376, which is beyond our character set. We leave it untouched. (This is the non-breaking space character.)

>>> prove $ \c -> toUpper (toUpper c) .== toUpper c
Q.E.D.
>>> prove $ \c -> isUpper c ==> toUpper (toLower c) .== c
Q.E.D.

Convert a digit to an integer. Works for hexadecimal digits too. If the input isn't a digit, then return -1.

>>> prove $ \c -> isDigit c ||| isHexDigit c ==> digitToInt c .>= 0 &&& digitToInt c .<= 15
Q.E.D.
>>> prove $ \c -> bnot (isDigit c ||| isHexDigit c) ==> digitToInt c .== -1
Q.E.D.

Convert an an integer to a digit, inverse of digitToInt. If the integer is out of bounds, we return the arbitrarily chosen space character. Note that for hexadecimal letters, we return the corresponding lowercase letter.

>>> prove $ \i -> i .>= 0 &&& i .<= 15 ==> digitToInt (intToDigit i) .== i
Q.E.D.
>>> prove $ \i -> i .<  0 ||| i .>  15 ==> digitToInt (intToDigit i) .== -1
Q.E.D.
>>> prove $ \c -> digitToInt c .== -1 <=> intToDigit (digitToInt c) .== literal ' '
Q.E.D.

Is this a control character? Control characters are essentially the non-printing characters.

Is this white-space? That is, one of "tnvfr 160".

Is this a lower-case character?

>>> prove $ \c -> isUpper c ==> isLower (toLower c)
Q.E.D.

Is this an upper-case character?

>>> prove $ \c -> bnot (isLower c &&& isUpper c)
Q.E.D.

Is this an alphabet character? That is lower-case, upper-case and title-case letters, plus letters of caseless scripts and modifiers letters.

Is this an isAlpha or isNumber.

>>> prove $ \c -> isAlphaNum c <=> isAlpha c ||| isNumber c
Q.E.D.

Is this a printable character? Essentially the complement of isControl, with one exception. The Latin-1 character 173 is neither control nor printable. Go figure.

>>> prove $ \c -> c .== literal '\173' ||| isControl c <=> bnot (isPrint c)
Q.E.D.

Is this an ASCII digit, i.e., one of 0..9. Note that this is a subset of isNumber

>>> prove $ \c -> isDigit c ==> isNumber c
Q.E.D.

Is this an Octal digit, i.e., one of 0..7.

>>> prove $ \c -> isOctDigit c ==> isDigit c
Q.E.D.

Is this a Hex digit, i.e, one of 0..9, a..f, A..F.

>>> prove $ \c -> isHexDigit c ==> isAlphaNum c
Q.E.D.

Is this an alphabet character. Note that this function is equivalent to isAlpha.

>>> prove $ \c -> isLetter c <=> isAlpha c
Q.E.D.

Is this a mark? Note that the Latin-1 subset doesn't have any marks; so this function is simply constant false for the time being.

>>> prove $ bnot . isMark
Q.E.D.

Is this a number character? Note that this set contains not only the digits, but also the codes for a few numeric looking characters like 1/2 etc. Use isDigit for the digits 0 through 9.

Is this a punctuation mark?

Is this a symbol?

Is this a separator?

>>> prove $ \c -> isSeparator c ==> isSpace c
Q.E.D.

Is this an ASCII character, i.e., the first 128 characters.

Is this a Latin1 character? Note that this function is always true since SChar corresponds precisely to Latin1 for the time being.

>>> prove isLatin1
Q.E.D.

Is this an ASCII letter?

>>> prove $ \c -> isAsciiLetter c <=> isAsciiUpper c ||| isAsciiLower c
Q.E.D.

Is this an ASCII Upper-case letter? i.e., A thru Z

>>> prove $ \c -> isAsciiUpper c <=> ord c .>= ord (literal 'A') &&& ord c .<= ord (literal 'Z')
Q.E.D.
>>> prove $ \c -> isAsciiUpper c <=> isAscii c &&& isUpper c
Q.E.D.

Is this an ASCII Lower-case letter? i.e., a thru z

>>> prove $ \c -> isAsciiLower c <=> ord c .>= ord (literal 'a') &&& ord c .<= ord (literal 'z')
Q.E.D.
>>> prove $ \c -> isAsciiLower c <=> isAscii c &&& isLower c
Q.E.D.