package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3
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 universes_entry = | Monomorphic_entry of Univ.ContextSet.t| Polymorphic_entry of Names.Name.t array * Univ.UContext.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 : universes_entry;mind_entry_template : bool;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_feedback : Stateid.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_feedback : Stateid.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_feedback : Stateid.t option;opaque_entry_type : Constr.types;opaque_entry_universes : universes_entry;
}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
older 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