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.10.0.0.7.2.tbz
sha256=39018932b0520cc042246a3f9e03f3788d1aaff65568b480d8681cba235032e9
sha512=62a3bb3950e5f9d9cfa5fca85a1108a04fd8c1833cba560ff9d52246ef96d3d61a4743e6dc6d52f53c6a495040fad53f1d9aae383609227a6eb84568ad2a1a6c

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

Module 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 =
  1. | Monomorphic_entry of Univ.ContextSet.t
  2. | Polymorphic_entry of Names.Name.t array * Univ.UContext.t
val universes_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> universes_entry
val sexp_of_universes_entry : universes_entry -> Ppx_sexp_conv_lib.Sexp.t
type 'a in_universes_entry = 'a * universes_entry
val in_universes_entry_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a in_universes_entry
val sexp_of_in_universes_entry : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a in_universes_entry -> Ppx_sexp_conv_lib.Sexp.t
type one_inductive_entry = Entries.one_inductive_entry = {
  1. mind_entry_typename : Names.Id.t;
  2. mind_entry_arity : Constr.constr;
  3. mind_entry_template : bool;
  4. mind_entry_consnames : Names.Id.t list;
  5. mind_entry_lc : Constr.constr list;
}
val one_inductive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> one_inductive_entry
val sexp_of_one_inductive_entry : one_inductive_entry -> Ppx_sexp_conv_lib.Sexp.t
type 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_variance : Univ.Variance.t array option;
  7. mind_entry_private : bool option;
}
val mutual_inductive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> mutual_inductive_entry
val sexp_of_mutual_inductive_entry : mutual_inductive_entry -> Ppx_sexp_conv_lib.Sexp.t
type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
val proof_output_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a proof_output
val sexp_of_proof_output : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a proof_output -> Ppx_sexp_conv_lib.Sexp.t
type 'a const_entry_body = 'a proof_output Future.computation
val const_entry_body_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a const_entry_body
val sexp_of_const_entry_body : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a const_entry_body -> Ppx_sexp_conv_lib.Sexp.t
type 'a definition_entry = 'a Entries.definition_entry = {
  1. const_entry_body : 'a const_entry_body;
  2. const_entry_secctx : Constr.named_context option;
  3. const_entry_feedback : Stateid.t option;
  4. const_entry_type : Constr.types option;
  5. const_entry_universes : universes_entry;
  6. const_entry_opaque : bool;
  7. const_entry_inline_code : bool;
}
val definition_entry_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a definition_entry
val sexp_of_definition_entry : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a definition_entry -> Ppx_sexp_conv_lib.Sexp.t
type section_def_entry = Entries.section_def_entry = {
  1. secdef_body : Constr.constr;
  2. secdef_secctx : Constr.named_context option;
  3. secdef_feedback : Stateid.t option;
  4. secdef_type : Constr.types option;
}
val section_def_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> section_def_entry
val sexp_of_section_def_entry : section_def_entry -> Ppx_sexp_conv_lib.Sexp.t
type inline = int option
val inline_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> inline
val sexp_of_inline : inline -> Ppx_sexp_conv_lib.Sexp.t
type parameter_entry = Constr.named_context option * Constr.types in_universes_entry * inline
val parameter_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> parameter_entry
val sexp_of_parameter_entry : parameter_entry -> Ppx_sexp_conv_lib.Sexp.t
type primitive_entry = Entries.primitive_entry = {
  1. prim_entry_type : Constr.types option;
  2. prim_entry_univs : Univ.ContextSet.t;
  3. prim_entry_content : CPrimitives.op_or_type;
}
val primitive_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> primitive_entry
val sexp_of_primitive_entry : primitive_entry -> Ppx_sexp_conv_lib.Sexp.t
type 'a constant_entry = 'a Entries.constant_entry =
  1. | DefinitionEntry of 'a definition_entry
  2. | ParameterEntry of parameter_entry
  3. | PrimitiveEntry of primitive_entry
val constant_entry_of_sexp : 'a. (Ppx_sexp_conv_lib.Sexp.t -> 'a) -> Ppx_sexp_conv_lib.Sexp.t -> 'a constant_entry
val sexp_of_constant_entry : 'a. ('a -> Ppx_sexp_conv_lib.Sexp.t) -> 'a constant_entry -> Ppx_sexp_conv_lib.Sexp.t
type module_struct_entry = Declarations.module_alg_expr
val module_struct_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_struct_entry
val sexp_of_module_struct_entry : module_struct_entry -> Ppx_sexp_conv_lib.Sexp.t
type module_params_entry = (Names.MBId.t * module_struct_entry) list
val module_params_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_params_entry
val sexp_of_module_params_entry : module_params_entry -> Ppx_sexp_conv_lib.Sexp.t
type 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
val module_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_entry
val sexp_of_module_entry : module_entry -> Ppx_sexp_conv_lib.Sexp.t
type module_type_entry = module_params_entry * module_struct_entry
val module_type_entry_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> module_type_entry
val sexp_of_module_type_entry : module_type_entry -> Ppx_sexp_conv_lib.Sexp.t
type seff_env = [
  1. | `Nothing
  2. | `Opaque of Constr.t * Univ.ContextSet.t
]
val __seff_env_of_sexp__ : Ppx_sexp_conv_lib.Sexp.t -> seff_env
val seff_env_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> seff_env
val sexp_of_seff_env : seff_env -> Ppx_sexp_conv_lib.Sexp.t
type side_effect_role = Entries.side_effect_role =
  1. | Subproof
  2. | Schema of Names.inductive * string
val side_effect_role_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> side_effect_role
val sexp_of_side_effect_role : side_effect_role -> Ppx_sexp_conv_lib.Sexp.t
type side_eff = Entries.side_eff = {
  1. seff_constant : Names.Constant.t;
  2. seff_body : Declarations.constant_body;
  3. seff_env : seff_env;
  4. seff_role : side_effect_role;
}
val side_eff_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> side_eff
val sexp_of_side_eff : side_eff -> 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