Module `Serlib.Ser_entries`Source

Sourcemodule Stateid = Ser_stateid

Sourcemodule Future = Ser_future

Sourcemodule Names = Ser_names

Sourcemodule Univ = Ser_univ

Sourcemodule Constr = Ser_constr

Sourcemodule Declarations = Ser_declarations

Sourcemodule CPrimitives = Ser_cPrimitives

Sourcetype universes_entry = Entries.universes_entry =

| Monomorphic_entry
| Polymorphic_entry of Univ.UContext.t

Sourceval universes_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> universes_entry

Sourceval sexp_of_universes_entry : universes_entry -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype 'a in_universes_entry = 'a * universes_entry

Source

val in_universes_entry_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a in_universes_entry

Source

val sexp_of_in_universes_entry : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a in_universes_entry ->
  Ppx_sexp_conv_lib.Sexp.t

Sourcetype one_inductive_entry = Entries.one_inductive_entry = {

mind_entry_typename : Names.Id.t;
mind_entry_arity : Constr.constr;
mind_entry_consnames : Names.Id.t list;
mind_entry_lc : Constr.constr list;

}

Source

val one_inductive_entry_of_sexp : 
  Ppx_sexp_conv_lib.Sexp.t ->
  one_inductive_entry

Source

val sexp_of_one_inductive_entry : 
  one_inductive_entry ->
  Ppx_sexp_conv_lib.Sexp.t

Sourcetype variance_entry = Univ.Variance.t option array

Sourceval variance_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> variance_entry

Sourceval sexp_of_variance_entry : variance_entry -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a

Source

val proof_output_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a proof_output

Source

val sexp_of_proof_output : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a proof_output ->
  Ppx_sexp_conv_lib.Sexp.t

Sourcetype definition_entry = Entries.definition_entry = {

const_entry_body : Constr.constr;
const_entry_secctx : Names.Id.Set.t option;
const_entry_type : Constr.types option;
const_entry_universes : universes_entry;
const_entry_inline_code : bool;

}

Sourceval definition_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> definition_entry

Sourceval sexp_of_definition_entry : definition_entry -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype section_def_entry = Entries.section_def_entry = {

secdef_body : Constr.constr;
secdef_secctx : Names.Id.Set.t option;
secdef_type : Constr.types option;

}

Sourceval section_def_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> section_def_entry

Sourceval sexp_of_section_def_entry : section_def_entry -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype inline = int option

Sourceval inline_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> inline

Sourceval sexp_of_inline : inline -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype 'a opaque_entry = 'a Entries.opaque_entry = {

opaque_entry_body : 'a;
opaque_entry_secctx : Names.Id.Set.t;
opaque_entry_type : Constr.types;
opaque_entry_universes : universes_entry;

}

Source

val opaque_entry_of_sexp : 
  'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) ->
  Ppx_sexp_conv_lib.Sexp.t ->
  'a opaque_entry

Source

val sexp_of_opaque_entry : 
  'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) ->
  'a opaque_entry ->
  Ppx_sexp_conv_lib.Sexp.t

Sourcetype parameter_entry = Entries.parameter_entry = {

parameter_entry_secctx : Names.Id.Set.t option;
parameter_entry_type : Constr.types;
parameter_entry_universes : universes_entry;
parameter_entry_inline_code : inline;

}

Sourceval parameter_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> parameter_entry

Sourceval sexp_of_parameter_entry : parameter_entry -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype primitive_entry = Entries.primitive_entry = {

prim_entry_type : Constr.types in_universes_entry option;
prim_entry_content : CPrimitives.op_or_type;

}

Sourceval primitive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> primitive_entry

Sourceval sexp_of_primitive_entry : primitive_entry -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype constant_entry = Entries.constant_entry =

| DefinitionEntry : definition_entry -> constant_entry
| ParameterEntry : parameter_entry -> constant_entry
| PrimitiveEntry : primitive_entry -> constant_entry

Sourceval constant_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> constant_entry

Sourceval sexp_of_constant_entry : constant_entry -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype module_struct_entry = Declarations.module_alg_expr

Source

val module_struct_entry_of_sexp : 
  Ppx_sexp_conv_lib.Sexp.t ->
  module_struct_entry

Source

val sexp_of_module_struct_entry : 
  module_struct_entry ->
  Ppx_sexp_conv_lib.Sexp.t

Sourcetype module_params_entry = (Names.MBId.t * module_struct_entry) list

Source

val module_params_entry_of_sexp : 
  Ppx_sexp_conv_lib.Sexp.t ->
  module_params_entry

Source

val sexp_of_module_params_entry : 
  module_params_entry ->
  Ppx_sexp_conv_lib.Sexp.t

Sourcetype 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

Sourceval module_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_entry

Sourceval sexp_of_module_entry : module_entry -> Ppx_sexp_conv_lib.Sexp.t

Sourcetype module_type_entry = module_params_entry * module_struct_entry

Sourceval module_type_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_type_entry

Sourceval sexp_of_module_type_entry : module_type_entry -> Ppx_sexp_conv_lib.Sexp.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-serapi.serlib/Serlib/Ser_entries/index.html

Module `Serlib.Ser_entries`Source

package coq-serapi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-serapi.serlib/Serlib/Ser_entries/index.html

Module Serlib.Ser_entriesSource

Module `Serlib.Ser_entries`Source