package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Big : a wrapper around ocaml ZArith with nicer names, and a few extraction-specific constructions

To be linked with zarith

type big_int = Z.t

The type of big integers.

val zero : Z.t

The big integer 0.

val one : Z.t

The big integer 1.

val two : Z.t

The big integer 2.

Arithmetic operations
val opp : Z.t -> Z.t

Unary negation.

val abs : Z.t -> Z.t

Absolute value.

val add : Z.t -> Z.t -> Z.t

Addition.

val succ : Z.t -> Z.t

Successor (add 1).

val add_int : Z.t -> Z.t -> Z.t

Addition of a small integer to a big integer.

val sub : Z.t -> Z.t -> Z.t

Subtraction.

val pred : Z.t -> Z.t

Predecessor (subtract 1).

val mult : Z.t -> Z.t -> Z.t

Multiplication of two big integers.

val mult_int : int -> Z.t -> Z.t

Multiplication of a big integer by a small integer

val square : Z.t -> Z.t

Return the square of the given big integer

val sqrt : Z.t -> Z.t

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.

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 have a = q * b + r and 0 <= r < |b|. Raise Division_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 of quomod_big_int (see above).

val modulo : Z.t -> Z.t -> Z.t

Euclidean modulus of two big integers. This is the second result r of quomod_big_int (see above).

val gcd : Z.t -> Z.t -> Z.t

Greatest common divisor of two big integers.

val power : Z.t -> int -> Z.t

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
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 returns 0 if a and b are equal, 1 if a is greater than b, and -1 if a is smaller than b.

val eq : Z.t -> Z.t -> bool
val le : Z.t -> Z.t -> bool
val ge : Z.t -> Z.t -> bool
val lt : Z.t -> Z.t -> bool
val gt : Z.t -> Z.t -> bool

Usual boolean comparisons between two big integers.

val max : Z.t -> Z.t -> Z.t

Return the greater of its two arguments.

val min : Z.t -> Z.t -> Z.t

Return the smaller of its two arguments.

Conversions to and from strings
val to_string : Z.t -> string

Return the string representation of the given big integer, in decimal (base 10).

val of_string : string -> Z.t

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
val of_int : int -> Z.t

Convert a small integer to a big integer.

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 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.

val to_int : Z.t -> int

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

val double : Z.t -> Z.t
val doubleplusone : Z.t -> Z.t
val nat_case : (unit -> 'a) -> (Z.t -> 'b) -> Z.t -> 'c
val positive_case : (Z.t -> 'a) -> (Z.t -> 'b) -> (unit -> 'c) -> Z.t -> 'd
val n_case : (unit -> 'a) -> (Z.t -> 'b) -> Z.t -> 'c
val z_case : (unit -> 'a) -> (Z.t -> 'b) -> (Z.t -> 'c) -> Z.t -> 'd
val compare_case : 'a -> 'b -> 'c -> Z.t -> Z.t -> 'd
val nat_rec : 'a -> ('b -> 'c) -> Z.t -> 'd
val positive_rec : ('a -> 'b) -> ('c -> 'd) -> 'e -> Z.t -> 'f
val z_rec : 'a -> (Z.t -> 'b) -> (Z.t -> 'b) -> Z.t -> 'b
OCaml

Innovation. Community. Security.