package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Stateid = Ser_stateid
module Future = Ser_future
module Names = Ser_names
module Univ = Ser_univ
module Constr = Ser_constr
module Declarations = Ser_declarations
type local_entry = Entries.local_entry =
  1. | LocalDefEntry of Constr.constr
  2. | LocalAssumEntry of Constr.constr
val local_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> local_entry
val sexp_of_local_entry : local_entry -> Ppx_sexp_conv_lib.Sexp.t
type inductive_universes = Entries.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
val inductive_universes_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> inductive_universes
val sexp_of_inductive_universes : inductive_universes -> Ppx_sexp_conv_lib.Sexp.t
type one_inductive_entry = Entries.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;
}
val one_inductive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> one_inductive_entry
val sexp_of_one_inductive_entry : one_inductive_entry -> Ppx_sexp_conv_lib.Sexp.t
type mutual_inductive_entry = Entries.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;
}
val mutual_inductive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> mutual_inductive_entry
val sexp_of_mutual_inductive_entry : mutual_inductive_entry -> Ppx_sexp_conv_lib.Sexp.t
type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
val proof_output_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a proof_output
val sexp_of_proof_output : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a proof_output -> Ppx_sexp_conv_lib.Sexp.t
type 'a const_entry_body = 'a proof_output Future.computation
val const_entry_body_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a const_entry_body
val sexp_of_const_entry_body : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a const_entry_body -> Ppx_sexp_conv_lib.Sexp.t
type constant_universes_entry = Entries.constant_universes_entry =
  1. | Monomorphic_const_entry of Univ.ContextSet.t
  2. | Polymorphic_const_entry of Univ.UContext.t
val constant_universes_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> constant_universes_entry
val sexp_of_constant_universes_entry : constant_universes_entry -> Ppx_sexp_conv_lib.Sexp.t
type 'a in_constant_universes_entry = 'a * constant_universes_entry
val in_constant_universes_entry_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a in_constant_universes_entry
val sexp_of_in_constant_universes_entry : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a in_constant_universes_entry -> Ppx_sexp_conv_lib.Sexp.t
type 'a definition_entry = 'a Entries.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;
}
val definition_entry_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a definition_entry
val sexp_of_definition_entry : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a definition_entry -> Ppx_sexp_conv_lib.Sexp.t
type section_def_entry = Entries.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;
}
val section_def_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> section_def_entry
val sexp_of_section_def_entry : section_def_entry -> Ppx_sexp_conv_lib.Sexp.t
type inline = int option
val inline_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> inline
val sexp_of_inline : inline -> Ppx_sexp_conv_lib.Sexp.t
type parameter_entry = Constr.named_context option * Constr.types in_constant_universes_entry * inline
val parameter_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> parameter_entry
val sexp_of_parameter_entry : parameter_entry -> Ppx_sexp_conv_lib.Sexp.t
type 'a constant_entry = 'a Entries.constant_entry =
  1. | DefinitionEntry of 'a definition_entry
  2. | ParameterEntry of parameter_entry
val constant_entry_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a constant_entry
val sexp_of_constant_entry : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a constant_entry -> Ppx_sexp_conv_lib.Sexp.t
type module_struct_entry = Declarations.module_alg_expr
val module_struct_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_struct_entry
val sexp_of_module_struct_entry : module_struct_entry -> Ppx_sexp_conv_lib.Sexp.t
type module_params_entry = (Names.MBId.t * module_struct_entry) list
val module_params_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_params_entry
val sexp_of_module_params_entry : module_params_entry -> Ppx_sexp_conv_lib.Sexp.t
type module_entry = Entries.module_entry =
  1. | MType of module_params_entry * module_struct_entry
  2. | MExpr of module_params_entry * module_struct_entry * module_struct_entry option
val module_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_entry
val sexp_of_module_entry : module_entry -> Ppx_sexp_conv_lib.Sexp.t
type module_type_entry = module_params_entry * module_struct_entry
val module_type_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_type_entry
val sexp_of_module_type_entry : module_type_entry -> Ppx_sexp_conv_lib.Sexp.t
type seff_env = [
  1. | `Nothing
  2. | `Opaque of Constr.t * Univ.ContextSet.t
]
val __seff_env_of_sexp__ : Ppx_sexp_conv_lib.Sexp.t -> seff_env
val seff_env_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> seff_env
val sexp_of_seff_env : seff_env -> Ppx_sexp_conv_lib.Sexp.t
type side_effect_role = Entries.side_effect_role =
  1. | Subproof
  2. | Schema of Names.inductive * string
val side_effect_role_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> side_effect_role
val sexp_of_side_effect_role : side_effect_role -> Ppx_sexp_conv_lib.Sexp.t
type side_eff = Entries.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;
}
val side_eff_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> side_eff
val sexp_of_side_eff : side_eff -> Ppx_sexp_conv_lib.Sexp.t