package coq

  1. Overview
  2. Docs
package coq
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct