package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type local_entry =
  1. | LocalDefEntry of Term.constr
  2. | LocalAssumEntry of Term.constr
type inductive_universes =
  1. | Monomorphic_ind_entry of Univ.universe_context
  2. | Polymorphic_ind_entry of Univ.universe_context
  3. | Cumulative_ind_entry of Univ.cumulativity_info
type one_inductive_entry = {
  1. mind_entry_typename : Names.Id.t;
  2. mind_entry_arity : Term.constr;
  3. mind_entry_template : bool;
  4. mind_entry_consnames : Names.Id.t list;
  5. mind_entry_lc : Term.constr list;
}
type mutual_inductive_entry = {
  1. mind_entry_record : Names.Id.t option option;
  2. mind_entry_finite : Decl_kinds.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 = Term.constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
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 : Term.types option;
  5. const_entry_polymorphic : bool;
  6. const_entry_universes : Univ.universe_context;
  7. const_entry_opaque : bool;
  8. const_entry_inline_code : bool;
}
type inline = int option
type parameter_entry = Context.Named.t option * bool * Term.types Univ.in_universe_context * inline
type projection_entry = {
  1. proj_entry_ind : Names.mutual_inductive;
  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.universe_context_set
]
type side_eff =
  1. | SEsubproof of Names.constant * Declarations.constant_body * seff_env
  2. | SEscheme of (Names.inductive * Names.constant * 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