package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type local_entry =
  1. | LocalDefEntry of Constr.constr
  2. | LocalAssumEntry of Constr.constr
type inductive_universes =
  1. | Monomorphic_ind_entry of Univ.ContextSet.t
  2. | Polymorphic_ind_entry of Univ.UContext.t
  3. | Cumulative_ind_entry of Univ.CumulativityInfo.t
type one_inductive_entry = {
  1. mind_entry_typename : Names.Id.t;
  2. mind_entry_arity : Constr.constr;
  3. mind_entry_template : bool;
  4. mind_entry_consnames : Names.Id.t list;
  5. 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 : (Names.Id.t * local_entry) list;
  4. mind_entry_inds : one_inductive_entry list;
  5. mind_entry_universes : inductive_universes;
  6. mind_entry_private : bool option;
}
type !'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
type constant_universes_entry =
  1. | Monomorphic_const_entry of Univ.ContextSet.t
  2. | Polymorphic_const_entry of Univ.UContext.t
type !'a in_constant_universes_entry = 'a * constant_universes_entry
type !'a definition_entry = {
  1. const_entry_body : 'a const_entry_body;
  2. const_entry_secctx : Constr.named_context option;
  3. const_entry_feedback : Stateid.t option;
  4. const_entry_type : Constr.types option;
  5. const_entry_universes : constant_universes_entry;
  6. const_entry_opaque : bool;
  7. const_entry_inline_code : bool;
}
type section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_secctx : Constr.named_context option;
  3. secdef_feedback : Stateid.t option;
  4. secdef_type : Constr.types option;
}
type inline = int option
type parameter_entry = Constr.named_context option * Constr.types in_constant_universes_entry * inline
type !'a constant_entry =
  1. | DefinitionEntry of 'a definition_entry
  2. | ParameterEntry of parameter_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
type seff_env = [
  1. | `Nothing
  2. | `Opaque of Constr.t * Univ.ContextSet.t
]
type side_effect_role =
  1. | Subproof
  2. | Schema of Names.inductive * string
type side_eff = {
  1. seff_constant : Names.Constant.t;
  2. seff_body : Declarations.constant_body;
  3. seff_env : seff_env;
  4. seff_role : side_effect_role;
}
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