package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/coq-core.kernel/Entries/index.html
Module EntriesSource
This module defines the entry types for global declarations. This information is entered in the environments. This includes global constants/axioms, mutual inductive definitions, modules and module types
Source
type inductive_universes_entry = | Monomorphic_ind_entry| Polymorphic_ind_entry of Univ.UContext.t| Template_ind_entry of Univ.ContextSet.t
Declaration of inductive types.
Assume the following definition in concrete syntax:
Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1 ... with Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
then, in ith block, mind_entry_params is xn:Xn;...;x1:X1; mind_entry_arity is Ai, defined in context x1:X1;...;xn:Xn; mind_entry_lc is Ti1;...;Tini, defined in context [A'1;...;A'p;x1:X1;...;xn:Xn] where A'i is Ai generalized over [x1:X1;...;xn:Xn].
Source
type one_inductive_entry = {mind_entry_typename : Names.Id.t;mind_entry_arity : Constr.constr;mind_entry_consnames : Names.Id.t list;mind_entry_lc : Constr.constr list;
}Source
type mutual_inductive_entry = {mind_entry_record : Names.Id.t array option option;(*Some (Some ids): primitive records with ids the binder name of each record in their respective projections. Not used by the kernel. Some None: non-primitive record
*)mind_entry_finite : Declarations.recursivity_kind;mind_entry_params : Constr.rel_context;mind_entry_inds : one_inductive_entry list;mind_entry_universes : inductive_universes_entry;mind_entry_variance : variance_entry option;mind_entry_private : bool option;
}Constants (Definition/Axiom)
Source
type definition_entry = {const_entry_body : Constr.constr;const_entry_secctx : Names.Id.Set.t option;const_entry_type : Constr.types option;const_entry_universes : universes_entry;const_entry_inline_code : bool;
}Source
type section_def_entry = {secdef_body : Constr.constr;secdef_secctx : Names.Id.Set.t option;secdef_type : Constr.types option;
}Source
type 'a opaque_entry = {opaque_entry_body : 'a;opaque_entry_secctx : Names.Id.Set.t;opaque_entry_type : Constr.types;opaque_entry_universes : universes_entry;
}Source
type parameter_entry = {parameter_entry_secctx : Names.Id.Set.t option;parameter_entry_type : Constr.types;parameter_entry_universes : universes_entry;parameter_entry_inline_code : inline;
}Source
type primitive_entry = {prim_entry_type : Constr.types in_universes_entry option;prim_entry_content : CPrimitives.op_or_type;
}Source
type constant_entry = | DefinitionEntry : definition_entry -> constant_entry| ParameterEntry : parameter_entry -> constant_entry| PrimitiveEntry : primitive_entry -> constant_entry
Modules
Source
type module_struct_entry =
(Constr.constr * Univ.AbstractContext.t option) Declarations.module_alg_exprolder first
Source
type module_entry = | MType of module_params_entry * module_struct_entry| MExpr of module_params_entry * module_struct_entry * module_struct_entry option