fact: Definition uint_of_char (a:ascii)(d:option uint) := match d with | None => None | Some d => match a with | "0" => Some (D0 d) | "1" => Some (D1 d) | "2" => Some (D2 d) | "3" => Some (D3 d) | "4" => Some (D4 d) | "5" => Some (D5 d) | "6" => Some (D6 d) | "7" => Some (D7 d) | "8" => Some (D8 d) | "9" => Some (D9 d) | "a" => Some (Da d) | "b" => Some (Db d) | "c" => Some (Dc d) | "d" => Some (Dd d) | "e" => Some (De d) | "f" => Some (Df d) | _ => None end end%char.
imports: Hexadecimal Ascii String