fact: Fixpoint readBinAux (s : string) (acc : nat) : option nat := match s with | "" => Some acc | String c s' => match binDigitToNat c with | Some n => readBinAux s' (2 * acc + n) | None => None end end.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.NArith.NArith