fact: Fixpoint to_N (s : string) (rest : N) : N := match s with | "" => rest | String ch s' => to_N s' match ascii_to_digit ch with | Some v => N.add v (N.double rest) | None => N0 end end.
imports: Ascii String BinNums