package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.0.tar.gz
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250

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