package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type set_predicativity =
  1. | ImpredicativeSet
  2. | PredicativeSet
type engagement = set_predicativity
type template_arity = {
  1. template_level : Univ.Universe.t;
}
type template_universes = {
  1. template_param_levels : Univ.Level.t option list;
  2. template_context : Univ.ContextSet.t;
}
type (!'a, !'b) declaration_arity =
  1. | RegularArity of 'a
  2. | TemplateArity of 'b
type inline = int option
type (!'a, !'opaque) constant_def =
  1. | Undef of inline
  2. | Def of 'a
  3. | OpaqueDef of 'opaque
  4. | Primitive of CPrimitives.t
type universes =
  1. | Monomorphic of Univ.ContextSet.t
  2. | Polymorphic of Univ.AUContext.t
type typing_flags = {
  1. check_guarded : bool;
  2. check_positive : bool;
  3. check_universes : bool;
  4. conv_oracle : Conv_oracle.oracle;
  5. share_reduction : bool;
  6. enable_VM : bool;
  7. enable_native_compiler : bool;
  8. indices_matter : bool;
  9. cumulative_sprop : bool;
  10. allow_uip : bool;
}
type !'opaque constant_body = {
  1. const_hyps : Constr.named_context;
  2. const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
  3. const_type : Constr.types;
  4. const_relevance : Sorts.relevance;
  5. const_body_code : Vmemitcodes.to_patch_substituted option;
  6. const_universes : universes;
  7. const_inline_code : bool;
  8. const_typing_flags : typing_flags;
}
type nested_type =
  1. | NestedInd of Names.inductive
  2. | NestedPrimitive of Names.Constant.t
type recarg =
  1. | Norec
  2. | Mrec of Names.inductive
  3. | Nested of nested_type
type wf_paths = recarg Rtree.t
type record_info =
  1. | NotRecord
  2. | FakeRecord
  3. | PrimRecord of (Names.Id.t * Names.Label.t array * Sorts.relevance array * Constr.types array) array
type regular_inductive_arity = {
  1. mind_user_arity : Constr.types;
  2. mind_sort : Sorts.t;
}
type one_inductive_body = {
  1. mind_typename : Names.Id.t;
  2. mind_arity_ctxt : Constr.rel_context;
  3. mind_arity : inductive_arity;
  4. mind_consnames : Names.Id.t array;
  5. mind_user_lc : Constr.types array;
  6. mind_nrealargs : int;
  7. mind_nrealdecls : int;
  8. mind_kelim : Sorts.family;
  9. mind_nf_lc : (Constr.rel_context * Constr.types) array;
  10. mind_consnrealargs : int array;
  11. mind_consnrealdecls : int array;
  12. mind_recargs : wf_paths;
  13. mind_relevance : Sorts.relevance;
  14. mind_nb_constant : int;
  15. mind_nb_args : int;
  16. mind_reloc_tbl : Vmvalues.reloc_table;
}
type recursivity_kind =
  1. | Finite
  2. | CoFinite
  3. | BiFinite
type mutual_inductive_body = {
  1. mind_packets : one_inductive_body array;
  2. mind_record : record_info;
  3. mind_finite : recursivity_kind;
  4. mind_ntypes : int;
  5. mind_hyps : Constr.named_context;
  6. mind_nparams : int;
  7. mind_nparams_rec : int;
  8. mind_params_ctxt : Constr.rel_context;
  9. mind_universes : universes;
  10. mind_template : template_universes option;
  11. mind_variance : Univ.Variance.t array option;
  12. mind_sec_variance : Univ.Variance.t array option;
  13. mind_private : bool option;
  14. mind_typing_flags : typing_flags;
}
type (!'ty, !'a) functorize =
  1. | NoFunctor of 'a
  2. | MoreFunctor of Names.MBId.t * 'ty * ('ty, 'a) functorize
type with_declaration =
  1. | WithMod of Names.Id.t list * Names.ModPath.t
  2. | WithDef of Names.Id.t list * Constr.constr * Univ.AUContext.t option
type module_alg_expr =
  1. | MEident of Names.ModPath.t
  2. | MEapply of module_alg_expr * Names.ModPath.t
  3. | MEwith of module_alg_expr * with_declaration
type structure_field_body =
  1. | SFBconst of Opaqueproof.opaque constant_body
  2. | SFBmind of mutual_inductive_body
  3. | SFBmodule of module_body
  4. | SFBmodtype of module_type_body
and structure_body = (Names.Label.t * structure_field_body) list
and module_signature = (module_type_body, structure_body) functorize
and module_expression = (module_type_body, module_alg_expr) functorize
and module_implementation =
  1. | Abstract
  2. | Algebraic of module_expression
  3. | Struct of module_signature
  4. | FullStruct
and !'a generic_module_body = {
  1. mod_mp : Names.ModPath.t;
  2. mod_expr : 'a;
  3. mod_type : module_signature;
  4. mod_type_alg : module_expression option;
  5. mod_delta : Mod_subst.delta_resolver;
  6. mod_retroknowledge : 'a module_retroknowledge;
}
and module_body = module_implementation generic_module_body
and module_type_body = unit generic_module_body
and !_ module_retroknowledge =
  1. | ModBodyRK : Retroknowledge.action list -> module_implementation module_retroknowledge
  2. | ModTypeRK : unit module_retroknowledge
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