package coq-core

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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 universes_entry =
  1. | Monomorphic_entry
  2. | Polymorphic_entry of Univ.UContext.t
type inductive_universes_entry =
  1. | Monomorphic_ind_entry
  2. | Polymorphic_ind_entry of Univ.UContext.t
  3. | Template_ind_entry of Univ.ContextSet.t
type variance_entry = Univ.Variance.t option array
type 'a in_universes_entry = 'a * universes_entry
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].

type one_inductive_entry = {
  1. mind_entry_typename : Names.Id.t;
  2. mind_entry_arity : Constr.constr;
  3. mind_entry_consnames : Names.Id.t list;
  4. mind_entry_lc : Constr.constr list;
}
type mutual_inductive_entry = {
  1. 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

    *)
  2. mind_entry_finite : Declarations.recursivity_kind;
  3. mind_entry_params : Constr.rel_context;
  4. mind_entry_inds : one_inductive_entry list;
  5. mind_entry_universes : inductive_universes_entry;
  6. mind_entry_variance : variance_entry option;
  7. mind_entry_private : bool option;
}
Constants (Definition/Axiom)
type definition_entry = {
  1. const_entry_body : Constr.constr;
  2. const_entry_secctx : Names.Id.Set.t option;
  3. const_entry_type : Constr.types option;
  4. const_entry_universes : universes_entry;
  5. const_entry_inline_code : bool;
}
type section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_type : Constr.types option;
}
type 'a opaque_entry = {
  1. opaque_entry_body : 'a;
  2. opaque_entry_secctx : Names.Id.Set.t;
  3. opaque_entry_type : Constr.types;
  4. opaque_entry_universes : universes_entry;
}
type inline = int option
type parameter_entry = {
  1. parameter_entry_secctx : Names.Id.Set.t option;
  2. parameter_entry_type : Constr.types;
  3. parameter_entry_universes : universes_entry;
  4. parameter_entry_inline_code : inline;
}
type primitive_entry = {
  1. prim_entry_type : Constr.types in_universes_entry option;
  2. prim_entry_content : CPrimitives.op_or_type;
}
type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
type constant_entry =
  1. | DefinitionEntry : definition_entry -> constant_entry
  2. | ParameterEntry : parameter_entry -> constant_entry
  3. | PrimitiveEntry : primitive_entry -> constant_entry
Modules
type module_params_entry = (Names.MBId.t * module_struct_entry * inline) list

older first

type module_type_entry = module_params_entry * module_struct_entry
OCaml

Innovation. Community. Security.