package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Extraction_plugin.BigSource

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

To be linked with zarith

Sourcetype big_int = Z.t

The type of big integers.

Sourceval zero : Z.t

The big integer 0.

Sourceval one : Z.t

The big integer 1.

Sourceval two : Z.t

The big integer 2.

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

Unary negation.

Sourceval abs : Z.t -> Z.t

Absolute value.

Sourceval add : Z.t -> Z.t -> Z.t

Addition.

Sourceval succ : Z.t -> Z.t

Successor (add 1).

Sourceval add_int : Z.t -> Z.t -> Z.t

Addition of a small integer to a big integer.

Sourceval sub : Z.t -> Z.t -> Z.t

Subtraction.

Sourceval pred : Z.t -> Z.t

Predecessor (subtract 1).

Sourceval mult : Z.t -> Z.t -> Z.t

Multiplication of two big integers.

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

Multiplication of a big integer by a small integer

Sourceval square : Z.t -> Z.t

Return the square of the given big integer

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

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

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

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

Sourceval gcd : Z.t -> Z.t -> Z.t

Greatest common divisor of two big integers.

Sourceval 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
Sourceval sign : Z.t -> int

Return 0 if the given big integer is zero, 1 if it is positive, and -1 if it is negative.

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

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

Usual boolean comparisons between two big integers.

Sourceval max : Z.t -> Z.t -> Z.t

Return the greater of its two arguments.

Sourceval min : Z.t -> Z.t -> Z.t

Return the smaller of its two arguments.

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

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

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

Convert a small integer to a big integer.

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

Sourceval 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

Sourceval double : Z.t -> Z.t
Sourceval doubleplusone : Z.t -> Z.t
Sourceval nat_case : (unit -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a
Sourceval positive_case : (Z.t -> 'a) -> (Z.t -> 'a) -> (unit -> 'a) -> Z.t -> 'a
Sourceval n_case : (unit -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a
Sourceval z_case : (unit -> 'a) -> (Z.t -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a
Sourceval compare_case : 'a -> 'a -> 'a -> Z.t -> Z.t -> 'a
Sourceval nat_rec : 'a -> ('a -> 'a) -> Z.t -> 'a
Sourceval positive_rec : ('a -> 'a) -> ('a -> 'a) -> 'a -> Z.t -> 'a
Sourceval z_rec : 'a -> (Z.t -> 'a) -> (Z.t -> 'a) -> Z.t -> 'a
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