fact: Definition ascii_to_digit (ch : ascii) : option N := (if ascii_dec ch "0" then Some 0 else if ascii_dec ch "1" then Some 1 else if ascii_dec ch "2" then Some 2 else if ascii_dec ch "3" then Some 3 else if ascii_dec ch "4" then Some 4 else if ascii_dec ch "5" then Some 5 else if ascii_dec ch "6" then Some 6 else if ascii_dec ch "7" then Some 7 else if ascii_dec ch "8" then Some 8 else if ascii_dec ch "9" then Some 9 else if ascii_dec ch "a" || ascii_dec ch "A" then Some 10 else if ascii_dec ch "b" || ascii_dec ch "B" then Some 11 else if ascii_dec ch "c" || ascii_dec ch "C" then Some 12 else if ascii_dec ch "d" || ascii_dec ch "D" then Some 13 else if ascii_dec ch "e" || ascii_dec ch "E" then Some 14 else if ascii_dec ch "f" || ascii_dec ch "F" then Some 15 else None)%N.
imports: Ascii String BinNums