From 960d48790121b876e6be7ca033138f5d28eae0cb Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 27 Feb 2017 19:56:27 +0100 Subject: Decimal: simple representation of base-10 numbers --- theories/ZArith/BinIntDef.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'theories/ZArith') diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 443667f48..a0393f318 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -299,6 +299,23 @@ Definition to_pos (z:Z) : positive := | _ => 1%positive end. +(** Conversion with a decimal representation for printing/parsing *) + +Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d). + +Definition of_int (d:Decimal.int) := + match d with + | Decimal.Pos d => of_uint d + | Decimal.Neg d => opp (of_uint d) + end. + +Definition to_int n := + match n with + | 0 => Decimal.Pos Decimal.zero + | pos p => Decimal.Pos (Pos.to_uint p) + | neg p => Decimal.Neg (Pos.to_uint p) + end. + (** ** Iteration of a function By convention, iterating a negative number of times is identity. -- cgit v1.2.3