diff options
Diffstat (limited to 'src/Util/Strings/Decimal.v')
-rw-r--r-- | src/Util/Strings/Decimal.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Util/Strings/Decimal.v b/src/Util/Strings/Decimal.v index 1a3c276e0..933c7648e 100644 --- a/src/Util/Strings/Decimal.v +++ b/src/Util/Strings/Decimal.v @@ -204,6 +204,24 @@ Proof. ... Qed.*) +Definition decimal_string_of_Z (v : Z) : string + := match v with + | Zpos p => decimal_string_of_pos p + | Z0 => "0" + | Zneg p => String "-" (decimal_string_of_pos p) + end. + +Definition Z_of_decimal_string (s : string) : Z + := if string_beq s "0" + then Z0 + else match s with + | String sgn v + => if ascii_beq sgn "-" + then Zneg (pos_of_decimal_string v) + else Zpos (pos_of_decimal_string s) + | _ => Zpos (pos_of_decimal_string s) + end. + Example decimal_string_of_pos_1 : decimal_string_of_pos 1 = "1" := eq_refl. Example decimal_string_of_pos_2 : decimal_string_of_pos 2 = "2" := eq_refl. Example decimal_string_of_pos_3 : decimal_string_of_pos 3 = "3" := eq_refl. |