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
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