ATSLIB/contrib/libats-hwxi/intinf_vt

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 that is also memory-efficient.

intinf

Intinf

Synopsis

vtypedef Intinf = [i:int] intinf (i)

intinfLt

Synopsis

vtypedef
intinfLt (i0:int) = [i:int | i < i0] intinf (i)

intinfLte

Synopsis

vtypedef
intinfLte (i0:int) = [i:int | i <= i0] intinf (i)

intinfGt

Synopsis

vtypedef
intinfGt (i0:int) = [i:int | i > i0] intinf (i)

intinfGte

Synopsis

vtypedef
intinfGte (i0:int) = [i:int | i >= i0] intinf (i)

intinfBtw

Synopsis

vtypedef
intinfBtw (i1:int, i2:int) = [i:int | i1 <= i; i < i2] intinf (i)

intinfBtwe

Synopsis

vtypedef
intinfBtwe (i1:int, i2:int) = [i:int | i1 <= i; i <= i2] intinf (i)

intinf_make_int

Synopsis

fun{}
intinf_make_int {i:int} (x: int (i)): intinf (i)

intinf_make_uint

Synopsis

fun{}
intinf_make_uint {i:int} (x: uint (i)): intinf (i)

intinf_make_lint

Synopsis

fun{}
intinf_make_lint {i:int} (x: lint (i)): intinf (i)

intinf_make_ulint

Synopsis

fun{}
intinf_make_ulint {i:int} (x: ulint (i)): intinf (i)

intinf_free

Synopsis

fun{}
intinf_free (x: Intinf): void

print_intinf

Synopsis

fun{}
print_intinf (x: !Intinf): void

prerr_intinf

Synopsis

fun{}
prerr_intinf (x: !Intinf): void

fprint_intinf

Synopsis

fun{}
fprint_intinf (out: FILEref, x: !Intinf): void

fprint_intinf_base

Synopsis

fun{}
fprint_intinf_base
  (out: FILEref, x: !Intinf, base: intinf_base): void

abs_intinf0

Synopsis

fun{}
abs_intinf0 {i:int} (x: intinf i): intinf (abs(i))

abs_intinf1

Synopsis

fun{}
abs_intinf1 {i:int} (x: !intinf i): intinf (abs(i))

neg_intinf0

Synopsis

fun{}
neg_intinf0 {i:int} (x: intinf i): intinf (~i)

neg_intinf1

Synopsis

fun{}
neg_intinf1 {i:int} (x: !intinf i): intinf (~i)

succ_intinf0

Synopsis

fun{}
succ_intinf0 {i:int} (x: intinf i): intinf (i+1)

succ_intinf1

Synopsis

fun{}
succ_intinf1 {i:int} (x: !intinf i): intinf (i+1)

pred_intinf0

Synopsis

fun{}
pred_intinf0 {i:int} (x: intinf i): intinf (i-1)

pred_intinf1

Synopsis

fun{}
pred_intinf1 {i:int} (x: !intinf i): intinf (i-1)

add_intinf0_int

Synopsis

fun{}
add_intinf0_int
  {i,j:int} (x: intinf i, y: int j): intinf (i+j)

add_intinf1_int

Synopsis

fun{}
add_intinf1_int
  {i,j:int} (x: !intinf i, y: int j): intinf (i+j)

add_int_intinf0

Synopsis

fun{}
add_int_intinf0
  {i,j:int} (x: int i, y: intinf j): intinf (i+j)

add_int_intinf1

Synopsis

fun{}
add_int_intinf1
  {i,j:int} (x: int i, y: !intinf j): intinf (i+j)

add_intinf0_intinf1

Synopsis

fun{}
add_intinf0_intinf1
  {i,j:int} (x: intinf i, y: !intinf j): intinf (i+j)

add_intinf1_intinf0

Synopsis

fun{}
add_intinf1_intinf0
  {i,j:int} (x: !intinf i, y: intinf j): intinf (i+j)

add_intinf1_intinf1

Synopsis

fun{}
add_intinf1_intinf1
  {i,j:int} (x: !intinf i, y: !intinf j): intinf (i+j)

sub_intinf0_int

Synopsis

fun{}
sub_intinf0_int
  {i,j:int} (x: intinf i, y: int j): intinf (i-j)

sub_intinf1_int

Synopsis

fun{}
sub_intinf1_int
  {i,j:int} (x: !intinf i, y: int j): intinf (i-j)

sub_int_intinf0

Synopsis

fun{}
sub_int_intinf0
  {i,j:int} (x: int i, y: intinf j): intinf (i-j)

sub_int_intinf1

Synopsis

fun{}
sub_int_intinf1
  {i,j:int} (x: int i, y: !intinf j): intinf (i-j)

sub_intinf0_intinf1

Synopsis

fun{}
sub_intinf0_intinf1
  {i,j:int} (x: intinf i, y: !intinf j): intinf (i-j)

sub_intinf1_intinf0

Synopsis

fun{}
sub_intinf1_intinf0
  {i,j:int} (x: !intinf i, y: intinf j): intinf (i-j)

sub_intinf1_intinf1

Synopsis

fun{}
sub_intinf1_intinf1
  {i,j:int} (x: !intinf i, y: !intinf j): intinf (i-j)

mul_intinf0_int

Synopsis

fun{}
mul_intinf0_int
  {i,j:int} (x: intinf i, y: int j): intinf (i*j)

mul_intinf1_int

Synopsis

fun{}
mul_intinf1_int
  {i,j:int} (x: !intinf i, y: int j): intinf (i*j)

mul_int_intinf0

Synopsis

fun{}
mul_int_intinf0
  {i,j:int} (x: int i, y: intinf j): intinf (i*j)

mul_int_intinf1

Synopsis

fun{}
mul_int_intinf1
  {i,j:int} (x: int i, y: !intinf j): intinf (i*j)

mul_intinf0_intinf1

Synopsis

fun{}
mul_intinf0_intinf1
  {i,j:int} (x: intinf i, y: !intinf j): intinf (i*j)

mul_intinf1_intinf0

Synopsis

fun{}
mul_intinf1_intinf0
  {i,j:int} (x: !intinf i, y: intinf j): intinf (i*j)

mul_intinf1_intinf1

Synopsis

fun{}
mul_intinf1_intinf1
  {i,j:int} (x: !intinf i, y: !intinf j): intinf (i*j)

div_intinf0_int

Synopsis

fun{}
div_intinf0_int
  {i,j:int | j != 0} (x: intinf i, y: int j): Intinf

div_intinf1_int

Synopsis

fun{}
div_intinf1_int
  {i,j:int | j != 0} (x: !intinf i, y: int j): Intinf

div_intinf0_intinf1

Synopsis

fun{}
div_intinf0_intinf1
  {i,j:int} (x: intinf i, y: !intinf j): Intinf

div_intinf1_intinf0

Synopsis

fun{}
div_intinf1_intinf0
  {i,j:int} (x: !intinf i, y: intinf j): Intinf

div_intinf1_intinf1

Synopsis

fun{}
div_intinf1_intinf1
  {i,j:int} (x: !intinf i, y: !intinf j): Intinf

ndiv_intinf0_int

Synopsis

fun{}
ndiv_intinf0_int
  {i,j:int | i >= 0; j > 0}
  (x: intinf i, y: int j): intinf (ndiv(i,j))

ndiv_intinf1_int

Synopsis

fun{}
ndiv_intinf1_int
  {i,j:int | i >= 0; j > 0}
  (x: !intinf i, y: int j): intinf (ndiv(i,j))

nmod_intinf0_int

Synopsis

fun{}
nmod_intinf0_int
  {i,j:int | i >= 0; j > 0} (x: intinf i, y: int j): natLt (j)

nmod_intinf1_int

Synopsis

fun{}
nmod_intinf1_int
  {i,j:int | i >= 0; j > 0} (x: !intinf i, y: int j): natLt (j)

compare_int_intinf

Synopsis

fun{}
compare_int_intinf
  {i,j:int} (x: int i, y: !intinf j):<> int (sgn(i-j))

compare_intinf_int

Synopsis

fun{}
compare_intinf_int
  {i,j:int} (x: !intinf i, y: int j):<> int (sgn(i-j))

compare_intinf_intinf

Synopsis

fun{}
compare_intinf_intinf
  {i,j:int} (x: !intinf i, y: !intinf j):<> int (sgn(i-j))

pow_intinf_int

Synopsis

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.