package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type universes_entry =
  1. | Monomorphic_entry of Univ.ContextSet.t
  2. | Polymorphic_entry of Names.Name.t array * Univ.UContext.t
type !'a in_universes_entry = 'a * universes_entry
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;
  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 : universes_entry;
  6. mind_entry_template : bool;
  7. mind_entry_cumulative : bool;
  8. mind_entry_private : bool option;
}
type definition_entry = {
  1. const_entry_body : Constr.constr;
  2. const_entry_secctx : Names.Id.Set.t option;
  3. const_entry_feedback : Stateid.t option;
  4. const_entry_type : Constr.types option;
  5. const_entry_universes : universes_entry;
  6. const_entry_inline_code : bool;
}
type section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_secctx : Names.Id.Set.t option;
  3. secdef_feedback : Stateid.t option;
  4. 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_feedback : Stateid.t option;
  4. opaque_entry_type : Constr.types;
  5. opaque_entry_universes : universes_entry;
}
type inline = int option
type parameter_entry = Names.Id.Set.t option * Constr.types in_universes_entry * inline
type primitive_entry = {
  1. prim_entry_type : Constr.types option;
  2. prim_entry_univs : Univ.ContextSet.t;
  3. prim_entry_content : CPrimitives.op_or_type;
}
type !'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
type constant_entry =
  1. | DefinitionEntry : definition_entry -> constant_entry
  2. | ParameterEntry : parameter_entry -> constant_entry
  3. | PrimitiveEntry : primitive_entry -> constant_entry
type module_struct_entry = Declarations.module_alg_expr
type module_params_entry = (Names.MBId.t * module_struct_entry) list
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