package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/coq-core.kernel/Entries/index.html
Module Entries
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
type inductive_universes_entry = | Monomorphic_ind_entry| Polymorphic_ind_entry of UVars.UContext.t| Template_ind_entry of Univ.ContextSet.t
type variance_entry = UVars.Variance.t option arraytype 'a in_universes_entry = 'a * universes_entryDeclaration 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].
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;
}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)
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;
}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;
}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;
}type primitive_entry = {prim_entry_type : Constr.types in_universes_entry option;prim_entry_content : CPrimitives.op_or_type;
}type symbol_entry = {symb_entry_type : Constr.types;symb_entry_unfold_fix : bool;symb_entry_universes : universes_entry;
}type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'atype constant_entry = | DefinitionEntry : definition_entry -> constant_entry| ParameterEntry : parameter_entry -> constant_entry| PrimitiveEntry : primitive_entry -> constant_entry| SymbolEntry : symbol_entry -> constant_entry
Modules
type module_struct_entry =
(Constr.constr * UVars.AbstractContext.t option) Declarations.module_alg_exprtype module_params_entry = (Names.MBId.t * module_struct_entry * inline) listolder first
type module_type_entry = module_params_entry * module_struct_entrytype module_entry = | MType of module_params_entry * module_struct_entry| MExpr of module_params_entry * module_struct_entry * module_struct_entry option