package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.11.0.0.11.0.tbz
sha256=59d38d716fda7cb1d89e2e1519c93d22deaf14da4f0f2feccd45886317f3424c
sha512=21b0ccaf75b497e13662c3fa2c618413dfccf6abfaabbab1d27926836447a0fcdc0e2a92929401359321018a4a867124caad27e9db52c4f3e5040aff698999ef
doc/coq-serapi.serlib/Serlib/Ser_entries/index.html
Module Serlib.Ser_entries
module Stateid = Ser_stateidmodule Future = Ser_futuremodule Names = Ser_namesmodule Univ = Ser_univmodule Constr = Ser_constrmodule Declarations = Ser_declarationsmodule CPrimitives = Ser_cPrimitivestype universes_entry = Entries.universes_entry = | Monomorphic_entry of Univ.ContextSet.t| Polymorphic_entry of Names.Name.t array * Univ.UContext.t
val universes_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> universes_entryval sexp_of_universes_entry : universes_entry -> Ppx_sexp_conv_lib.Sexp.ttype 'a in_universes_entry = 'a * universes_entryval in_universes_entry_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a in_universes_entryval sexp_of_in_universes_entry :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a in_universes_entry ->
Ppx_sexp_conv_lib.Sexp.ttype one_inductive_entry = Entries.one_inductive_entry = {mind_entry_typename : Names.Id.t;mind_entry_arity : Constr.constr;mind_entry_template : bool;mind_entry_consnames : Names.Id.t list;mind_entry_lc : Constr.constr list;
}val one_inductive_entry_of_sexp :
Ppx_sexp_conv_lib.Sexp.t ->
one_inductive_entryval sexp_of_one_inductive_entry :
one_inductive_entry ->
Ppx_sexp_conv_lib.Sexp.ttype mutual_inductive_entry = Entries.mutual_inductive_entry = {mind_entry_record : Names.Id.t array option option;mind_entry_finite : Declarations.recursivity_kind;mind_entry_params : Constr.rel_context;mind_entry_inds : one_inductive_entry list;mind_entry_universes : universes_entry;mind_entry_variance : Univ.Variance.t array option;mind_entry_private : bool option;
}val mutual_inductive_entry_of_sexp :
Ppx_sexp_conv_lib.Sexp.t ->
mutual_inductive_entryval sexp_of_mutual_inductive_entry :
mutual_inductive_entry ->
Ppx_sexp_conv_lib.Sexp.ttype 'a proof_output = Constr.constr Univ.in_universe_context_set * 'aval proof_output_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a proof_outputval sexp_of_proof_output :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a proof_output ->
Ppx_sexp_conv_lib.Sexp.ttype 'a const_entry_body = 'a proof_output Future.computationval const_entry_body_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a const_entry_bodyval sexp_of_const_entry_body :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a const_entry_body ->
Ppx_sexp_conv_lib.Sexp.ttype definition_entry = Entries.definition_entry = {const_entry_body : Constr.constr;const_entry_secctx : Names.Id.Set.t option;const_entry_feedback : Stateid.t option;const_entry_type : Constr.types option;const_entry_universes : universes_entry;const_entry_inline_code : bool;
}val definition_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> definition_entryval sexp_of_definition_entry : definition_entry -> Ppx_sexp_conv_lib.Sexp.ttype section_def_entry = Entries.section_def_entry = {secdef_body : Constr.constr;secdef_secctx : Names.Id.Set.t option;secdef_feedback : Stateid.t option;secdef_type : Constr.types option;
}val section_def_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> section_def_entryval sexp_of_section_def_entry : section_def_entry -> Ppx_sexp_conv_lib.Sexp.tval inline_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> inlineval sexp_of_inline : inline -> Ppx_sexp_conv_lib.Sexp.ttype 'a opaque_entry = 'a Entries.opaque_entry = {opaque_entry_body : 'a;opaque_entry_secctx : Names.Id.Set.t;opaque_entry_feedback : Stateid.t option;opaque_entry_type : Constr.types;opaque_entry_universes : universes_entry;
}val opaque_entry_of_sexp :
'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
Ppx_sexp_conv_lib.Sexp.t ->
'a opaque_entryval sexp_of_opaque_entry :
'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
'a opaque_entry ->
Ppx_sexp_conv_lib.Sexp.ttype parameter_entry =
Names.Id.Set.t option * Constr.types in_universes_entry * inlineval parameter_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> parameter_entryval sexp_of_parameter_entry : parameter_entry -> Ppx_sexp_conv_lib.Sexp.ttype primitive_entry = Entries.primitive_entry = {prim_entry_type : Constr.types option;prim_entry_univs : Univ.ContextSet.t;prim_entry_content : CPrimitives.op_or_type;
}val primitive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> primitive_entryval sexp_of_primitive_entry : primitive_entry -> Ppx_sexp_conv_lib.Sexp.ttype constant_entry = Entries.constant_entry = | DefinitionEntry : definition_entry -> constant_entry| ParameterEntry : parameter_entry -> constant_entry| PrimitiveEntry : primitive_entry -> constant_entry
val constant_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> constant_entryval sexp_of_constant_entry : constant_entry -> Ppx_sexp_conv_lib.Sexp.ttype module_struct_entry = Declarations.module_alg_exprval module_struct_entry_of_sexp :
Ppx_sexp_conv_lib.Sexp.t ->
module_struct_entryval sexp_of_module_struct_entry :
module_struct_entry ->
Ppx_sexp_conv_lib.Sexp.ttype module_params_entry = (Names.MBId.t * module_struct_entry) listval module_params_entry_of_sexp :
Ppx_sexp_conv_lib.Sexp.t ->
module_params_entryval sexp_of_module_params_entry :
module_params_entry ->
Ppx_sexp_conv_lib.Sexp.ttype module_entry = Entries.module_entry = | MType of module_params_entry * module_struct_entry| MExpr of module_params_entry * module_struct_entry * module_struct_entry option
val module_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_entryval sexp_of_module_entry : module_entry -> Ppx_sexp_conv_lib.Sexp.ttype module_type_entry = module_params_entry * module_struct_entryval module_type_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_type_entryval sexp_of_module_type_entry : module_type_entry -> Ppx_sexp_conv_lib.Sexp.t