digitToInt package:sbv

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 -> sNot (isDigit c .|| isHexDigit c) .=> digitToInt c .== -1
Q.E.D.