This package is for supporting integers of unlimited precision, and it is implemented based on the GMP library. The primary purpose of the package is to provide a simple and clean approach to programming with large integers.
stadef intinf = intinf_type
typedef Intinf = [i:int] intinf (i)
typedef intinfLt (i0:int) = [i:int | i < i0] intinf (i)
typedef intinfLte (i0:int) = [i:int | i <= i0] intinf (i)
typedef intinfGt (i0:int) = [i:int | i > i0] intinf (i)
typedef intinfGte (i0:int) = [i:int | i >= i0] intinf (i)
typedef intinfBtw (i1:int, i2:int) = [i:int | i1 <= i; i < i2] intinf (i)
typedef intinfBtwe (i1:int, i2:int) = [i:int | i1 <= i; i <= i2] intinf (i)
fun{}
intinf_make_int {i:int} (x: int (i)): intinf (i)
fun{}
intinf_make_uint {i:int} (x: uint (i)): intinf (i)
fun{}
intinf_make_lint {i:int} (x: lint (i)): intinf (i)
fun{}
intinf_make_ulint {i:int} (x: ulint (i)): intinf (i)
Synopsis for [intinf_free] is unavailable.
fun{}
print_intinf (x: Intinf): void
fun{}
prerr_intinf (x: Intinf): void
fun{}
fprint_intinf (out: FILEref, x: Intinf): void
fun{}
fprint_intinf_base
(out: FILEref, x: Intinf, base: intinf_base): void
fun{}
abs_intinf {i:int} (x: intinf i): intinf (abs(i))
fun{}
neg_intinf {i:int} (x: intinf i): intinf (~i)
Synopsis for [succ_intinf1] is unavailable.
Synopsis for [pred_intinf1] is unavailable.
fun{}
add_intinf_int
{i,j:int} (x: intinf i, y: int j): intinf (i+j)
fun{}
add_int_intinf
{i,j:int} (x: int i, y: intinf j): intinf (i+j)
fun{}
add_intinf_intinf
{i,j:int} (x: intinf i, y: intinf j): intinf (i+j)
fun{}
sub_intinf_int
{i,j:int} (x: intinf i, y: int j): intinf (i-j)
fun{}
sub_int_intinf
{i,j:int} (x: int i, y: intinf j): intinf (i-j)
fun{}
sub_intinf_intinf
{i,j:int} (x: intinf i, y: intinf j): intinf (i-j)
fun{}
mul_intinf_int
{i,j:int} (x: intinf i, y: int j): intinf (i*j)
fun{}
mul_int_intinf
{i,j:int} (x: int i, y: intinf j): intinf (i*j)
fun{}
mul_intinf_intinf
{i,j:int} (x: intinf i, y: intinf j): intinf (i*j)
fun{}
compare_int_intinf
{i,j:int} (x: int i, y: intinf j):<> int (sgn(i-j))
fun{}
compare_intinf_int
{i,j:int} (x: intinf i, y: int j):<> int (sgn(i-j))
fun{}
compare_intinf_intinf
{i,j:int} (x: intinf i, y: intinf j):<> int (sgn(i-j))
fun{}
pow_intinf_int
{i:nat} (base: Intinf, exp: int i): Intinf
| This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. |
|