Module Extraction_plugin.Big
Arithmetic operations
val sqrt : Z.t -> Z.tsqrt_big_int areturns the integer square root ofa, that is, the largest big integerrsuch thatr * r <= a. RaiseInvalid_argumentifais negative.
val quomod : Z.t -> Z.t -> Z.t * Z.tEuclidean division of two big integers. The first part of the result is the quotient, the second part is the remainder. Writing
(q,r) = quomod_big_int a b, we havea = q * b + rand0 <= r < |b|. RaiseDivision_by_zeroif the divisor is zero.
val div : Z.t -> Z.t -> Z.tEuclidean quotient of two big integers. This is the first result
qofquomod_big_int(see above).
Comparisons and tests
val sign : Z.t -> intReturn
0if the given big integer is zero,1if it is positive, and-1if it is negative.
val compare : Z.t -> Z.t -> intcompare_big_int a breturns0ifaandbare equal,1ifais greater thanb, and-1ifais smaller thanb.
Conversions to and from strings
Conversions to and from other numerical types
val is_int : Z.t -> boolTest whether the given big integer is small enough to be representable as a small integer (type
int) without loss of precision. On a 32-bit platform,is_int_big_int areturnstrueif and only ifais between 230 and 230-1. On a 64-bit platform,is_int_big_int areturnstrueif and only ifais between -262 and 262-1.
val to_int : Z.t -> intConvert a big integer to a small integer (type
int). RaisesFailure "int_of_big_int"if the big integer is not representable as a small integer.
val double : Z.t -> Z.tval doubleplusone : Z.t -> Z.tval nat_case : (unit -> 'a) -> (Z.t -> 'a) -> Z.t -> 'aval positive_case : (Z.t -> 'a) -> (Z.t -> 'a) -> (unit -> 'a) -> Z.t -> 'aval n_case : (unit -> 'a) -> (Z.t -> 'a) -> Z.t -> 'aval z_case : (unit -> 'a) -> (Z.t -> 'a) -> (Z.t -> 'a) -> Z.t -> 'aval compare_case : 'a -> 'a -> 'a -> Z.t -> Z.t -> 'aval nat_rec : 'a -> ('a -> 'a) -> Z.t -> 'aval positive_rec : ('a -> 'a) -> ('a -> 'a) -> 'a -> Z.t -> 'aval z_rec : 'a -> (Z.t -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a