package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.library/Rocqlib/index.html
Module RocqlibSource
Indirection between logical names and global references.
This module provides a mechanism to bind “names” to constants and to look up these constants using their names.
The two main functions are register_ref n r which binds the name n to the reference r and lib_ref n which returns the previously registered reference under name n.
The first function is meant to be available through the vernacular command Register r as n, so that plug-ins can refer to a constant without knowing its user-facing name, the precise module path in which it is defined, etc.
For instance, lib_ref "core.eq.type" returns the proper GlobRef.t for the type of the core equality type.
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
type rocq_sigma_data = {proj1 : Names.GlobRef.t;proj2 : Names.GlobRef.t;elim : Names.GlobRef.t;intro : Names.GlobRef.t;typ : Names.GlobRef.t;
}type 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