package coq-serapi

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

Install

Dune Dependency

Authors

Maintainers

Sources

coq-serapi-8.13.0.0.13.0.tbz
sha256=ddef1d7278021ce391f62e8e222e10962c7a308d6a2dfd8320382b4cf9a8cd75
sha512=8ee9cc09e5b8708b6cd7b0af8fccaa900413aa106cb47d99ca1fdd5b39c52676fa906204766f8f9e0964cc7e3ef987009de79f26b534b2021cf66f20c3d62bfe

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

Module Serlib.Ser_genargSource

Sourcetype rlevel = Genarg.rlevel
Sourcetype glevel = Genarg.glevel
Sourcetype tlevel = Genarg.tlevel
Sourceval rlevel_of_sexp : Sexplib.Sexp.t -> rlevel
Sourceval sexp_of_rlevel : rlevel -> Sexplib.Sexp.t
Sourceval glevel_of_sexp : Sexplib.Sexp.t -> glevel
Sourceval sexp_of_glevel : glevel -> Sexplib.Sexp.t
Sourceval tlevel_of_sexp : Sexplib.Sexp.t -> tlevel
Sourceval sexp_of_tlevel : tlevel -> Sexplib.Sexp.t
Sourcetype 'a generic_argument = 'a Genarg.generic_argument
Sourceval generic_argument_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a Genarg.generic_argument
Sourceval sexp_of_generic_argument : ('a -> Sexplib.Sexp.t) -> 'a Genarg.generic_argument -> Sexplib.Sexp.t
Sourcetype glob_generic_argument = Genarg.glob_generic_argument
Sourceval glob_generic_argument_of_sexp : Sexplib.Sexp.t -> Genarg.glob_generic_argument
Sourceval sexp_of_glob_generic_argument : Genarg.glob_generic_argument -> Sexplib.Sexp.t
Sourcetype raw_generic_argument = Genarg.raw_generic_argument
Sourceval raw_generic_argument_of_sexp : Sexplib.Sexp.t -> Genarg.raw_generic_argument
Sourceval sexp_of_raw_generic_argument : Genarg.raw_generic_argument -> Sexplib.Sexp.t
Sourceval raw_generic_argument_of_yojson : Yojson.Safe.t -> (raw_generic_argument, string) Result.result
Sourceval raw_generic_argument_to_yojson : raw_generic_argument -> Yojson.Safe.t
Sourcetype typed_generic_argument = Genarg.typed_generic_argument
Sourceval typed_generic_argument_of_sexp : Sexplib.Sexp.t -> Genarg.typed_generic_argument
Sourceval sexp_of_typed_generic_argument : Genarg.typed_generic_argument -> Sexplib.Sexp.t
Sourcetype ('raw, 'glb, 'top) gen_ser = {
  1. raw_ser : 'raw -> Sexplib.Sexp.t;
  2. raw_des : Sexplib.Sexp.t -> 'raw;
  3. glb_ser : 'glb -> Sexplib.Sexp.t;
  4. glb_des : Sexplib.Sexp.t -> 'glb;
  5. top_ser : 'top -> Sexplib.Sexp.t;
  6. top_des : Sexplib.Sexp.t -> 'top;
}
Sourceval register_genser : ('raw, 'glb, 'top) Genarg.genarg_type -> ('raw, 'glb, 'top) gen_ser -> unit
Sourceval gen_ser_pair : ('raw1, 'glb1, 'top1) gen_ser -> ('raw2, 'glb2, 'top2) gen_ser -> ('raw1 * 'raw2, 'glb1 * 'glb2, 'top1 * 'top2) gen_ser
Sourceval gen_ser_list : ('raw, 'glb, 'top) gen_ser -> ('raw list, 'glb list, 'top list) gen_ser
Sourceval mk_uniform : ('t -> Sexplib.Sexp.t) -> (Sexplib.Sexp.t -> 't) -> ('t, 't, 't) gen_ser
OCaml

Innovation. Community. Security.