package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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_secctx : Names.Id.Set.t option;
  3. 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_struct_entry = (Constr.constr * Univ.AbstractContext.t option) Declarations.module_alg_expr
type module_params_entry = (Names.MBId.t * module_struct_entry * inline) list

older first

type module_type_entry = module_params_entry * module_struct_entry
type module_entry =
  1. | MType of module_params_entry * module_struct_entry
  2. | MExpr of module_params_entry * module_struct_entry * module_struct_entry option
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct