package coq-serapi

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

Install

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