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 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 : Context.Named.t 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 : Context.Named.t option;
  3. secdef_feedback : Stateid.t option;
  4. secdef_type : Constr.types option;
}
type inline = int option
type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline
type projection_entry = {
  1. proj_entry_ind : Names.MutInd.t;
  2. proj_entry_arg : int;
}
type !'a constant_entry =
  1. | DefinitionEntry of 'a definition_entry
  2. | ParameterEntry of parameter_entry
  3. | ProjectionEntry of projection_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_eff =
  1. | SEsubproof of Names.Constant.t * Declarations.constant_body * seff_env
  2. | SEscheme of (Names.inductive * Names.Constant.t * Declarations.constant_body * seff_env) list * string
type side_effect = {
  1. from_env : Declarations.structure_body CEphemeron.key;
  2. eff : side_eff;
}
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