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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.clib/Hashcons/index.html

Module HashconsSource

Generic hash-consing.

Hashconsing functorial interface
Sourcemodule type HashconsedType = sig ... end
Sourcemodule type S = sig ... end
Sourcemodule Make (X : HashconsedType) : S with type t = X.t and type u = X.u

Create a new hashconsing, given canonicalization functions.

Wrappers

These are intended to be used together with instances of the Make functor.

Sourceval simple_hcons : ('u -> 'tab) -> ('tab -> 't -> 't) -> 'u -> 't -> 't

simple_hcons f sub obj creates a new table each time it is applied to any sub-hash function sub.

Hashconsing of usual structures
Sourcemodule type HashedType = sig ... end
Sourcemodule Hstring : S with type t = string and type u = unit

Hashconsing of strings.

Sourcemodule Hlist (D : HashedType) : S with type t = D.t list and type u = D.t -> D.t

Hashconsing of lists.