package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
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;
}