package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

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

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz
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.

Sourceval register_ref : Libobject.locality -> string -> Names.GlobRef.t -> unit

Registers a global reference under the given name.

Sourceexception NotFoundRef of string
Sourceval lib_ref : string -> Names.GlobRef.t

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.

Sourceval lib_ref_opt : string -> Names.GlobRef.t option

As lib_ref but returns None instead of raising.

Sourceval has_ref : string -> bool

Checks whether a name refers to a registered constant. For any name n, if has_ref n returns true, lib_ref n will succeed.

Sourceval check_ref : string -> Names.GlobRef.t -> bool

Checks whether a name is bound to a known reference.

Sourceval check_ind_ref : string -> Names.inductive -> bool

Checks whether a name is bound to a known inductive.

Sourceval get_lib_refs : unit -> (string * Names.GlobRef.t) list

List of all currently bound names.

For Equality tactics

Sourcetype rocq_sigma_data = {
  1. proj1 : Names.GlobRef.t;
  2. proj2 : Names.GlobRef.t;
  3. elim : Names.GlobRef.t;
  4. intro : Names.GlobRef.t;
  5. typ : Names.GlobRef.t;
}
Sourceval build_sigma_type : rocq_sigma_data Util.delayed
Sourcetype rocq_eq_data = {
  1. eq : Names.GlobRef.t;
  2. ind : Names.GlobRef.t;
  3. refl : Names.GlobRef.t;
  4. sym : Names.GlobRef.t;
  5. trans : Names.GlobRef.t;
  6. congr : Names.GlobRef.t;
}
Sourceval build_rocq_eq_data : rocq_eq_data Util.delayed
Sourceval build_rocq_identity_data : rocq_eq_data Util.delayed
Sourceval build_rocq_jmeq_data : rocq_eq_data Util.delayed
Sourceval check_required_library : string list -> unit

For tactics/commands requiring vernacular libraries

Sourceval datatypes_module_name : string list
Sourceval logic_module_name : string list
Sourceval jmeq_module_name : string list