fact: Definition to_Z (s : string) : Z := let '(is_neg, n) := match s with | String s0 s' => if ascii_dec s0 "-" then (true, to_N s') else (false, to_N s) | EmptyString => (false, to_N s) end in match n with | N0 => Z0 | Npos p => if is_neg then Zneg p else Zpos p end.
imports: Ascii String BinNums