package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.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