package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4
doc/rocq-runtime.library/Coqlib/index.html
Module CoqlibSource
Deprecated alias for Rocqlib
include module type of struct include Rocqlib end
Registers a global reference under the given name.
Retrieves the reference bound to the given name (by a previous call to register_ref). Raises NotFoundRef if no reference is bound to this name.
As lib_ref but returns None instead of raising.
Checks whether a name refers to a registered constant. For any name n, if has_ref n returns true, lib_ref n will succeed.
Checks whether a name is bound to a known reference.
Checks whether a name is bound to a known inductive.
List of all currently bound names.
For Equality tactics
Source
type rocq_sigma_data = Rocqlib.rocq_sigma_data = {proj1 : Names.GlobRef.t;proj2 : Names.GlobRef.t;elim : Names.GlobRef.t;intro : Names.GlobRef.t;typ : Names.GlobRef.t;
}Source
type rocq_eq_data = Rocqlib.rocq_eq_data = {eq : Names.GlobRef.t;ind : Names.GlobRef.t;refl : Names.GlobRef.t;sym : Names.GlobRef.t;trans : Names.GlobRef.t;congr : Names.GlobRef.t;
}For tactics/commands requiring vernacular libraries
Source
type coq_sigma_data = rocq_sigma_data = {proj1 : Names.GlobRef.t;proj2 : Names.GlobRef.t;elim : Names.GlobRef.t;intro : Names.GlobRef.t;typ : Names.GlobRef.t;
}Source
type coq_eq_data = rocq_eq_data = {eq : Names.GlobRef.t;ind : Names.GlobRef.t;refl : Names.GlobRef.t;sym : Names.GlobRef.t;trans : Names.GlobRef.t;congr : Names.GlobRef.t;
}