Hashcons (rocq-runtime.Hashcons)

module type HashconsedType = sig ... end

module type HashconsedRecType = sig ... end

module type S = sig ... end

module Make (X : HashconsedType) : S with type t = X.t

Create a new hashconsing, given canonicalization functions.

module MakeRec (X : HashconsedRecType) : S with type t = X.t

Create a new hashconsing, given canonicalization functions. hashcons will get the resulting hcons as first argument.

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

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

Typically used as let hcons = simple_hcons H.generate H.hcons () where H is of type S.

module type HashedType = sig ... end

module Hlist (D : HashedType) : S with type t = D.t list

Hashconsing of lists.