Serlib.Ser_entries
module Stateid = Ser_stateid
module Future = Ser_future
module Names = Ser_names
module Univ = Ser_univ
module Constr = Ser_constr
module Declarations = Ser_declarations
module CPrimitives = Ser_cPrimitives
type universes_entry = Entries.universes_entry =
| Monomorphic_entry
| Polymorphic_entry of Univ.UContext.t
val universes_entry_of_sexp : Sexplib0.Sexp.t -> universes_entry
val sexp_of_universes_entry : universes_entry -> Sexplib0.Sexp.t
type 'a in_universes_entry = 'a * universes_entry
val in_universes_entry_of_sexp :
'a. (Sexplib0.Sexp.t -> 'a) ->
Sexplib0.Sexp.t ->
'a in_universes_entry
val sexp_of_in_universes_entry :
'a. ('a -> Sexplib0.Sexp.t) ->
'a in_universes_entry ->
Sexplib0.Sexp.t
type 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;
}
val one_inductive_entry_of_sexp : Sexplib0.Sexp.t -> one_inductive_entry
val sexp_of_one_inductive_entry : one_inductive_entry -> Sexplib0.Sexp.t
type variance_entry = Univ.Variance.t option array
val variance_entry_of_sexp : Sexplib0.Sexp.t -> variance_entry
val sexp_of_variance_entry : variance_entry -> Sexplib0.Sexp.t
type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
val proof_output_of_sexp :
'a. (Sexplib0.Sexp.t -> 'a) ->
Sexplib0.Sexp.t ->
'a proof_output
val sexp_of_proof_output :
'a. ('a -> Sexplib0.Sexp.t) ->
'a proof_output ->
Sexplib0.Sexp.t
type 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;
}
val definition_entry_of_sexp : Sexplib0.Sexp.t -> definition_entry
val sexp_of_definition_entry : definition_entry -> Sexplib0.Sexp.t
type section_def_entry = Entries.section_def_entry = {
secdef_body : Constr.constr;
secdef_secctx : Names.Id.Set.t option;
secdef_type : Constr.types option;
}
val section_def_entry_of_sexp : Sexplib0.Sexp.t -> section_def_entry
val sexp_of_section_def_entry : section_def_entry -> Sexplib0.Sexp.t
val inline_of_sexp : Sexplib0.Sexp.t -> inline
val sexp_of_inline : inline -> Sexplib0.Sexp.t
type '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;
}
val opaque_entry_of_sexp :
'a. (Sexplib0.Sexp.t -> 'a) ->
Sexplib0.Sexp.t ->
'a opaque_entry
val sexp_of_opaque_entry :
'a. ('a -> Sexplib0.Sexp.t) ->
'a opaque_entry ->
Sexplib0.Sexp.t
type 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;
}
val parameter_entry_of_sexp : Sexplib0.Sexp.t -> parameter_entry
val sexp_of_parameter_entry : parameter_entry -> Sexplib0.Sexp.t
type primitive_entry = Entries.primitive_entry = {
prim_entry_type : Constr.types in_universes_entry option;
prim_entry_content : CPrimitives.op_or_type;
}
val primitive_entry_of_sexp : Sexplib0.Sexp.t -> primitive_entry
val sexp_of_primitive_entry : primitive_entry -> Sexplib0.Sexp.t
type 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 : Sexplib0.Sexp.t -> constant_entry
val sexp_of_constant_entry : constant_entry -> Sexplib0.Sexp.t
type module_struct_entry =
(Constr.constr * Univ.AbstractContext.t option) Declarations.module_alg_expr
val module_struct_entry_of_sexp : Sexplib0.Sexp.t -> module_struct_entry
val sexp_of_module_struct_entry : module_struct_entry -> Sexplib0.Sexp.t
type module_params_entry = (Names.MBId.t * module_struct_entry * inline) list
val module_params_entry_of_sexp : Sexplib0.Sexp.t -> module_params_entry
val sexp_of_module_params_entry : module_params_entry -> Sexplib0.Sexp.t
type 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 : Sexplib0.Sexp.t -> module_entry
val sexp_of_module_entry : module_entry -> Sexplib0.Sexp.t
type module_type_entry = module_params_entry * module_struct_entry
val module_type_entry_of_sexp : Sexplib0.Sexp.t -> module_type_entry
val sexp_of_module_type_entry : module_type_entry -> Sexplib0.Sexp.t