package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
doc/extraction_plugin/Extraction_plugin/Big/index.html
Module Extraction_plugin.Big
Source
Big
: a wrapper around ocaml ZArith
with nicer names, and a few extraction-specific constructions
To be linked with zarith
The type of big integers.
The big integer 0
.
The big integer 1
.
The big integer 2
.
Arithmetic operations
Unary negation.
Absolute value.
Addition.
Successor (add 1).
Addition of a small integer to a big integer.
Subtraction.
Predecessor (subtract 1).
Multiplication of two big integers.
Multiplication of a big integer by a small integer
Return the square of the given big integer
sqrt_big_int a
returns the integer square root of a
, that is, the largest big integer r
such that r * r <= a
. Raise Invalid_argument
if a
is negative.
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 have a = q * b + r
and 0 <= r < |b|
. Raise Division_by_zero
if the divisor is zero.
Euclidean quotient of two big integers. This is the first result q
of quomod_big_int
(see above).
Euclidean modulus of two big integers. This is the second result r
of quomod_big_int
(see above).
Greatest common divisor of two big integers.
Exponentiation functions. Return the big integer representing the first argument a
raised to the power b
(the second argument). Depending on the function, a
and b
can be either small integers or big integers. Raise Invalid_argument
if b
is negative.
Comparisons and tests
Return 0
if the given big integer is zero, 1
if it is positive, and -1
if it is negative.
compare_big_int a b
returns 0
if a
and b
are equal, 1
if a
is greater than b
, and -1
if a
is smaller than b
.
Usual boolean comparisons between two big integers.
Return the greater of its two arguments.
Return the smaller of its two arguments.
Conversions to and from strings
Return the string representation of the given big integer, in decimal (base 10).
Convert a string to a big integer, in decimal. The string consists of an optional -
or +
sign, followed by one or several decimal digits.
Conversions to and from other numerical types
Convert a small integer to a big integer.
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
returns true
if and only if a
is between 230 and 230-1. On a 64-bit platform, is_int_big_int a
returns true
if and only if a
is between -262 and 262-1.
Convert a big integer to a small integer (type int
). Raises Failure "int_of_big_int"
if the big integer is not representable as a small integer.
Functions used by extraction