package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val uint_size : int
val maxuint31 : t
val of_int : int -> t
val to_int2 : t -> int * int
val of_int64 : Int64.t -> t
val to_int64 : t -> Int64.t

int_min n m returns the minimum of n and m, m must be in 0, 2^30-1.

val to_int_min : t -> int -> int

int_min n m returns the minimum of n and m, m must be in 0, 2^30-1.

val of_float : float -> t
val to_float : t -> float
val hash : t -> int
val to_string : t -> string
val compile : t -> string
val zero : t
val one : t
val l_sl : t -> t -> t
val l_sr : t -> t -> t
val l_and : t -> t -> t
val l_xor : t -> t -> t
val l_or : t -> t -> t
val a_sr : t -> t -> t
val add : t -> t -> t
val sub : t -> t -> t
val mul : t -> t -> t
val div : t -> t -> t
val rem : t -> t -> t
val diveucl : t -> t -> t * t
val divs : t -> t -> t
val rems : t -> t -> t
val mulc : t -> t -> t * t
val addmuldiv : t -> t -> t -> t
val div21 : t -> t -> t -> t * t

div21 xh xl y returns q % 2^63, r s.t. xh * 2^63 + xl = q * y + r and r < y. When y is 0, returns 0, 0.

val lt : t -> t -> bool
val equal : t -> t -> bool
val le : t -> t -> bool
val compare : t -> t -> int
val lts : t -> t -> bool
val les : t -> t -> bool
val compares : t -> t -> int
val head0 : t -> t
val tail0 : t -> t
val is_uint63 : Obj.t -> bool
type 'a carry =
  1. | C0 of 'a
  2. | C1 of 'a
val addc : t -> t -> t carry
val addcarryc : t -> t -> t carry
val subc : t -> t -> t carry
val subcarryc : t -> t -> t carry
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