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.18.0.0.18.3.tbz
sha256=d9a32c0033d720032011e9bf5e8d30d4b205ce276b6a81ab359fc461809e9b63
sha512=742d2b92b986e45044c19cd2bbfd5dd5346cfb4b0ec20f40811d8b0096c6e25192528359f98d2eed2a74ae67790d1f8cea382cb01fd7cf8903a5a917cca79a84

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
  2. | Polymorphic_entry of Univ.UContext.t
Sourceval universes_entry_of_sexp : Sexplib0.Sexp.t -> universes_entry
Sourceval sexp_of_universes_entry : universes_entry -> Sexplib0.Sexp.t
Sourcetype 'a in_universes_entry = 'a * universes_entry
Sourceval in_universes_entry_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a in_universes_entry
Sourceval sexp_of_in_universes_entry : 'a. ('a -> Sexplib0.Sexp.t) -> 'a in_universes_entry -> Sexplib0.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 : Sexplib0.Sexp.t -> one_inductive_entry
Sourceval sexp_of_one_inductive_entry : one_inductive_entry -> Sexplib0.Sexp.t
Sourcetype variance_entry = Univ.Variance.t option array
Sourceval variance_entry_of_sexp : Sexplib0.Sexp.t -> variance_entry
Sourceval sexp_of_variance_entry : variance_entry -> Sexplib0.Sexp.t
Sourceval proof_output_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a proof_output
Sourceval sexp_of_proof_output : 'a. ('a -> Sexplib0.Sexp.t) -> 'a proof_output -> Sexplib0.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_type : Constr.types option;
  4. const_entry_universes : universes_entry;
  5. const_entry_inline_code : bool;
}
Sourceval definition_entry_of_sexp : Sexplib0.Sexp.t -> definition_entry
Sourceval sexp_of_definition_entry : definition_entry -> Sexplib0.Sexp.t
Sourcetype section_def_entry = Entries.section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_type : Constr.types option;
}
Sourceval section_def_entry_of_sexp : Sexplib0.Sexp.t -> section_def_entry
Sourceval sexp_of_section_def_entry : section_def_entry -> Sexplib0.Sexp.t
Sourcetype inline = int option
Sourceval inline_of_sexp : Sexplib0.Sexp.t -> inline
Sourceval sexp_of_inline : inline -> Sexplib0.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_type : Constr.types;
  4. opaque_entry_universes : universes_entry;
}
Sourceval opaque_entry_of_sexp : 'a. (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a opaque_entry
Sourceval sexp_of_opaque_entry : 'a. ('a -> Sexplib0.Sexp.t) -> 'a opaque_entry -> Sexplib0.Sexp.t
Sourcetype parameter_entry = Entries.parameter_entry = {
  1. parameter_entry_secctx : Names.Id.Set.t option;
  2. parameter_entry_type : Constr.types;
  3. parameter_entry_universes : universes_entry;
  4. parameter_entry_inline_code : inline;
}
Sourceval parameter_entry_of_sexp : Sexplib0.Sexp.t -> parameter_entry
Sourceval sexp_of_parameter_entry : parameter_entry -> Sexplib0.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 : Sexplib0.Sexp.t -> primitive_entry
Sourceval sexp_of_primitive_entry : primitive_entry -> Sexplib0.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 : Sexplib0.Sexp.t -> constant_entry
Sourceval sexp_of_constant_entry : constant_entry -> Sexplib0.Sexp.t
Sourcetype module_struct_entry = (Constr.constr * Univ.AbstractContext.t option) Declarations.module_alg_expr
Sourceval module_struct_entry_of_sexp : Sexplib0.Sexp.t -> module_struct_entry
Sourceval sexp_of_module_struct_entry : module_struct_entry -> Sexplib0.Sexp.t
Sourcetype module_params_entry = (Names.MBId.t * module_struct_entry * inline) list
Sourceval module_params_entry_of_sexp : Sexplib0.Sexp.t -> module_params_entry
Sourceval sexp_of_module_params_entry : module_params_entry -> Sexplib0.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 : Sexplib0.Sexp.t -> module_entry
Sourceval sexp_of_module_entry : module_entry -> Sexplib0.Sexp.t
Sourcetype module_type_entry = module_params_entry * module_struct_entry
Sourceval module_type_entry_of_sexp : Sexplib0.Sexp.t -> module_type_entry
Sourceval sexp_of_module_type_entry : module_type_entry -> Sexplib0.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