package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.13.0.0.13.1.tbz
sha256=530991b3e029102367184b96d8bd8a347c7172265a5815176a533b1061f8c6cf
sha512=c6cc5afcad3546c3fbcd8512f20a5ebd748f17529805c1d296959092fde8f31b77f7c7a06254f68c30eb6c6ad520bfbf03388505186a600e75d65ae3acd02c77

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

Module Serlib.Ser_entriesSource

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 =
  1. | Monomorphic_entry of Univ.ContextSet.t
  2. | Polymorphic_entry of Names.Name.t array * 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
Sourceval in_universes_entry_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a in_universes_entry
Sourceval 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 = {
  1. mind_entry_typename : Names.Id.t;
  2. mind_entry_arity : Constr.constr;
  3. mind_entry_consnames : Names.Id.t list;
  4. mind_entry_lc : Constr.constr list;
}
Sourceval one_inductive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> one_inductive_entry
Sourceval 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 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 : Constr.rel_context;
  4. mind_entry_inds : one_inductive_entry list;
  5. mind_entry_universes : universes_entry;
  6. mind_entry_template : bool;
  7. mind_entry_variance : variance_entry option;
  8. mind_entry_private : bool option;
}
Sourceval mutual_inductive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> mutual_inductive_entry
Sourceval sexp_of_mutual_inductive_entry : mutual_inductive_entry -> Ppx_sexp_conv_lib.Sexp.t
Sourceval proof_output_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a proof_output
Sourceval sexp_of_proof_output : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a proof_output -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype 'a const_entry_body = 'a proof_output Future.computation
Sourceval const_entry_body_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a const_entry_body
Sourceval sexp_of_const_entry_body : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a const_entry_body -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype definition_entry = Entries.definition_entry = {
  1. const_entry_body : Constr.constr;
  2. const_entry_secctx : Names.Id.Set.t option;
  3. const_entry_feedback : Stateid.t option;
  4. const_entry_type : Constr.types option;
  5. const_entry_universes : universes_entry;
  6. 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 = {
  1. secdef_body : Constr.constr;
  2. secdef_secctx : Names.Id.Set.t option;
  3. secdef_feedback : Stateid.t option;
  4. 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 = {
  1. opaque_entry_body : 'a;
  2. opaque_entry_secctx : Names.Id.Set.t;
  3. opaque_entry_feedback : Stateid.t option;
  4. opaque_entry_type : Constr.types;
  5. opaque_entry_universes : universes_entry;
}
Sourceval opaque_entry_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a opaque_entry
Sourceval sexp_of_opaque_entry : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a opaque_entry -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype parameter_entry = Names.Id.Set.t option * Constr.types in_universes_entry * 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 = {
  1. prim_entry_type : Constr.types in_universes_entry option;
  2. 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 =
  1. | DefinitionEntry : definition_entry -> constant_entry
  2. | ParameterEntry : parameter_entry -> constant_entry
  3. | 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
Sourceval module_struct_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_struct_entry
Sourceval 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
Sourceval module_params_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_params_entry
Sourceval sexp_of_module_params_entry : module_params_entry -> Ppx_sexp_conv_lib.Sexp.t
Sourcetype 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
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