package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

dune-project

Dependency

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

Authors

T

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

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.0.tar.gz

sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

doc/coq-core.clib/Hashset/index.html

Module `Hashset`Source

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 = {

num_bindings : int;
num_buckets : int;
max_bucket_length : int;
bucket_histogram : int array;

}

Sourcemodule type S = sig ... end

Sourcemodule Make (E : EqType) : S with type elt = E.t

Sourcemodule Combine : sig ... end