package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/coq-core.kernel/Uint63/index.html

Module Uint63Source

Sourcetype t
Sourceval uint_size : int
Sourceval maxuint31 : t
Sourceval of_int : int -> t
Sourceval to_int2 : t -> int * int
Sourceval of_int64 : Int64.t -> t
Sourceval to_int64 : t -> Int64.t

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

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

Sourceval of_float : float -> t
Sourceval to_float : t -> float
Sourceval hash : t -> int
Sourceval to_string : t -> string
Sourceval compile : t -> string
Sourceval zero : t
Sourceval one : t
Sourceval l_sl : t -> t -> t
Sourceval l_sr : t -> t -> t
Sourceval l_and : t -> t -> t
Sourceval l_xor : t -> t -> t
Sourceval l_or : t -> t -> t
Sourceval a_sr : t -> t -> t
Sourceval add : t -> t -> t
Sourceval sub : t -> t -> t
Sourceval mul : t -> t -> t
Sourceval div : t -> t -> t
Sourceval rem : t -> t -> t
Sourceval diveucl : t -> t -> t * t
Sourceval divs : t -> t -> t
Sourceval rems : t -> t -> t
Sourceval mulc : t -> t -> t * t
Sourceval addmuldiv : t -> t -> t -> t
Sourceval 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.

Sourceval lt : t -> t -> bool
Sourceval equal : t -> t -> bool
Sourceval le : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval lts : t -> t -> bool
Sourceval les : t -> t -> bool
Sourceval compares : t -> t -> int
Sourceval head0 : t -> t
Sourceval tail0 : t -> t
Sourceval is_uint63 : Obj.t -> bool
Sourcetype 'a carry =
  1. | C0 of 'a
  2. | C1 of 'a
Sourceval addc : t -> t -> t carry
Sourceval addcarryc : t -> t -> t carry
Sourceval subc : t -> t -> t carry
Sourceval subcarryc : t -> t -> t carry