package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b
doc/coq-core.library/Coqlib/index.html
Module CoqlibSource
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 an error if no reference is bound to this name.
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 inductive.
List of all currently bound names.
For Equality tactics
type coq_sigma_data = {proj1 : Names.GlobRef.t;proj2 : Names.GlobRef.t;elim : Names.GlobRef.t;intro : Names.GlobRef.t;typ : Names.GlobRef.t;
}type coq_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
DEPRECATED
All the functions below are deprecated and should go away in the next coq version ...
find_reference caller_message [dir;subdir;...] s returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that it must be used lazily; it raises an anomaly with the given message if not found
This just prefixes find_reference with Coq...
Search in several modules (not prefixed by "Coq")
Global references
Modules
Identity
Natural numbers
Booleans
Equality
...
Constructions and patterns related to Coq initial state are unknown at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the constr delayed and constr_pattern delayed types. Objects of this time needs to be forced with delayed_force to get the actual constr or pattern at runtime.
type coq_bool_data = {andb : Names.GlobRef.t;andb_prop : Names.GlobRef.t;andb_true_intro : Names.GlobRef.t;
}Non-dependent pairs in Set from Datatypes
= (build_coq_eq_data()).eq
= (build_coq_eq_data()).refl
= (build_coq_eq_data()).sym
Data needed for discriminate and injection
type coq_inversion_data = {inv_eq : Names.GlobRef.t;(*: forall params, args -> Prop
*)inv_ind : Names.GlobRef.t;(*: forall params P (H : P params) args, eq params args -> P args
*)inv_congr : Names.GlobRef.t;(*: forall params B (f:t->B) args, eq params args -> f params = f args
*)
}Specif
...
Connectives The False proposition
The True proposition and its unique proof
Negation
Conjunction
Pairs
Disjunction
Existential quantifier