fact: Definition is_nat (x : ascii) : option nat := match x with | "0" => Some 0 | "1" => Some 1 | "2" => Some 2 | "3" => Some 3 | "4" => Some 4 | "5" => Some 5 | "6" => Some 6 | "7" => Some 7 | "8" => Some 8 | "9" => Some 9 | _ => None end%char.
imports: Coq(Ascii) stdpp(countable) stdpp(options)