Module Extraction_plugin.Big
Arithmetic operations
val sqrt : Z.t -> Z.t
sqrt_big_int a
returns the integer square root ofa
, that is, the largest big integerr
such thatr * r <= a
. RaiseInvalid_argument
ifa
is negative.
val quomod : Z.t -> Z.t -> Z.t * Z.t
Euclidean 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 + r
and0 <= r < |b|
. RaiseDivision_by_zero
if the divisor is zero.
val div : Z.t -> Z.t -> Z.t
Euclidean quotient of two big integers. This is the first result
q
ofquomod_big_int
(see above).
Comparisons and tests
val sign : Z.t -> int
Return
0
if the given big integer is zero,1
if it is positive, and-1
if it is negative.
val compare : Z.t -> Z.t -> int
compare_big_int a b
returns0
ifa
andb
are equal,1
ifa
is greater thanb
, and-1
ifa
is smaller thanb
.
Conversions to and from strings
Conversions to and from other numerical types
val is_int : Z.t -> bool
Test 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 a
returnstrue
if and only ifa
is between 230 and 230-1. On a 64-bit platform,is_int_big_int a
returnstrue
if and only ifa
is between -262 and 262-1.
val to_int : Z.t -> int
Convert 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.t
val doubleplusone : Z.t -> Z.t
val nat_case : (unit -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a
val positive_case : (Z.t -> 'a) -> (Z.t -> 'a) -> (unit -> 'a) -> Z.t -> 'a
val n_case : (unit -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a
val z_case : (unit -> 'a) -> (Z.t -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a
val compare_case : 'a -> 'a -> 'a -> Z.t -> Z.t -> 'a
val nat_rec : 'a -> ('a -> 'a) -> Z.t -> 'a
val positive_rec : ('a -> 'a) -> ('a -> 'a) -> 'a -> Z.t -> 'a
val z_rec : 'a -> (Z.t -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a