package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

dune-project

Dependency

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

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

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

Sources

rocq-9.0.1.tar.gz

sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.kernel/HConstr/index.html

Module `HConstr`Source

Sourcetype t

Hashconsed constr in an implicit environment, keeping variables which have different types and bodies separate.

For instance the x subterms in fun x : bool => x and fun x : nat => x are different (and have different hashes modulo accidental collision) and the x subterms in fun (y:nat) (x:bool) => x and fun (x:bool) (y:nat) => x are different (one is Rel 1, the other is Rel 2) but the x subterms in fun (y:nat) (x:bool) => x and fun (y:bool) (x:bool) => x are shared.

This allows using it as a cache key while typechecking.

Hashconsing information of subterms is also kept.

Sourceval self : t -> Constr.constr

Source

val kind : 
  t ->
  (t, t, Sorts.t, UVars.Instance.t, Sorts.relevance) Constr.kind_of_term

Sourceval refcount : t -> int

How many times this term appeared as a subterm of the argument to of_constr.

Sourceval of_constr : Environ.env -> Constr.constr -> t

Source

val of_kind_nohashcons : 
  (t, t, Sorts.t, UVars.Instance.t, Sorts.relevance) Constr.kind_of_term ->
  t

Build a t without hashconsing. Its refcount may be 1 even if an identical term was already seen.

May not be used to build Rel.

This is intended for the reconstruction of the inductive type when checking CaseInvert.

Sourcemodule Tbl : sig ... end

Imperative tables indexed by HConstr.t. The interfaces exposed are the same as Hashtbl but are not guaranteed to be implemented by Hashtbl.

Sourceval hcons : t -> Constr.t