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.clib/Hashset/index.html

Module HashsetSource

Adapted from Damien Doligez, projet Para, INRIA Rocquencourt, OCaml stdlib.

The following functor is a specialized version of Weak.Make. Here, the responsibility of computing the hash function is now given to the caller, which makes possible the interleaving of the hash key computation and the hash-consing.

Sourcemodule type EqType = sig ... end
Sourcetype statistics = {
  1. num_bindings : int;
  2. num_buckets : int;
  3. max_bucket_length : int;
  4. bucket_histogram : int array;
}
Sourcemodule type S = sig ... end
Sourcemodule Make (E : EqType) : S with type elt = E.t
Sourcemodule Combine : sig ... end