package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/coq-core.kernel/Names/index.html
Module Names
Source
This file defines a lot of different notions of names used pervasively in the kernel as well as in other places. The essential datatypes exported by this API are:
- Id.t is the type of identifiers, that is morally a subset of strings which only contains Unicode characters of the Letter kind (and a few more).
- Name.t is an ad-hoc variant of Id.t option allowing to handle optionally named objects.
- DirPath.t represents generic paths as sequences of identifiers.
- Label.t is an equivalent of Id.t made distinct for semantical purposes.
- ModPath.t are module paths.
- KerName.t are absolute names of objects in Coq.
Identifiers
Representation and operations on identifiers that are allowed to be anonymous (i.e. "_" in concrete syntax).
Type aliases
module ModIdset : Util.Set.S with type elt = module_ident
module ModIdmap :
Util.Map.ExtS with type key = module_ident and module Set := ModIdset
Directory paths = section names paths
module DPset : Util.Set.S with type elt = DirPath.t
Names of structure elements
Unique names for bound modules
module MBIset : Util.Set.S with type elt = MBId.t
The module part of the kernel name
module MPset : Util.Set.S with type elt = ModPath.t
The absolute names of objects seen by kernel
module KNpred : Predicate.S with type elt = KerName.t
Signature for quotiented names
Constant Names
module Cpred : Predicate.S with type elt = Constant.t
The *_env
modules consider an order on user part of names the others consider an order on canonical part of names
module Cset : CSig.SetS with type elt = Constant.t
module Cset_env : CSig.SetS with type elt = Constant.t
A map whose keys are constants (values of the Constant.t
type). Keys are ordered wrt. "canonical form" of the constant.
A map whose keys are constants (values of the Constant.t
type). Keys are ordered wrt. "user form" of the constant.
Inductive names
module Mindmap_env : CMap.ExtS with type key = MutInd.t
module Constrset : CSet.S with type elt = constructor
module Indset_env : CSet.S with type elt = inductive
module Constrset_env : CSet.S with type elt = constructor
module Indmap_env :
CMap.ExtS with type key = inductive and module Set := Indset_env
module Constrmap_env :
CMap.ExtS with type key = constructor and module Set := Constrset_env
Hash-consing
index in the rel_context
part of environment starting by the end, inverse of de Bruijn indice
equalities on constant and inductive names (for the checker)
Module paths
Global reference is a kernel side type for all references together
Located identifiers and objects with syntax.
- Identifiers
- Type aliases
- Directory paths = section names paths
- Names of structure elements
- Unique names for bound modules
- The module part of the kernel name
- The absolute names of objects seen by kernel
- Signature for quotiented names
- Constant Names
- Inductive names
- Hash-consing
- Module paths
- Global reference is a kernel side type for all references together