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.20.0.0.20.0.tbz
sha256=ead9382f111ea385008fe9037513ff1f738dd90d8e989b8d1a0c9290963d9afe
sha512=b29103c2d1eb3cf8a33fa9ddf26b5a6c89e7277cd31256589bcae8a89c37a3de7a3c3e7fe5d376358e874d44dc6c60ab96736cbd1037511ab36705e9f40f0ade

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

Module Serlib.Ser_genargSource

Sourcetype rlevel = Genarg.rlevel
Sourceval sexp_of_rlevel : rlevel -> Sexplib0.Sexp.t
Sourceval rlevel_of_sexp : Sexplib0.Sexp.t -> rlevel
Sourceval rlevel_to_yojson : rlevel -> Yojson.Safe.t
Sourceval hash_fold_rlevel : Ppx_hash_lib.Std.Hash.state -> rlevel -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_rlevel : rlevel -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_rlevel : rlevel -> rlevel -> int
Sourcetype glevel = Genarg.glevel
Sourceval sexp_of_glevel : glevel -> Sexplib0.Sexp.t
Sourceval glevel_of_sexp : Sexplib0.Sexp.t -> glevel
Sourceval glevel_to_yojson : glevel -> Yojson.Safe.t
Sourceval hash_fold_glevel : Ppx_hash_lib.Std.Hash.state -> glevel -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glevel : glevel -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glevel : glevel -> glevel -> int
Sourcetype tlevel = Genarg.tlevel
Sourceval sexp_of_tlevel : tlevel -> Sexplib0.Sexp.t
Sourceval tlevel_of_sexp : Sexplib0.Sexp.t -> tlevel
Sourceval tlevel_to_yojson : tlevel -> Yojson.Safe.t
Sourceval hash_fold_tlevel : Ppx_hash_lib.Std.Hash.state -> tlevel -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_tlevel : tlevel -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_tlevel : tlevel -> tlevel -> int
Sourcetype 'a generic_argument = 'a Genarg.generic_argument
Sourceval sexp_of_generic_argument : ('a -> Sexplib0.Sexp.t) -> 'a generic_argument -> Sexplib0.Sexp.t
Sourceval generic_argument_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a generic_argument
Sourceval generic_argument_to_yojson : ('a -> Yojson.Safe.t) -> 'a generic_argument -> Yojson.Safe.t
Sourceval hash_fold_generic_argument : (Ppx_hash_lib.Std.Hash.state -> 'a -> Ppx_hash_lib.Std.Hash.state) -> Ppx_hash_lib.Std.Hash.state -> 'a generic_argument -> Ppx_hash_lib.Std.Hash.state
Sourceval compare_generic_argument : ('a -> 'a -> int) -> 'a generic_argument -> 'a generic_argument -> int
Sourcetype glob_generic_argument = Genarg.glob_generic_argument
Sourceval sexp_of_glob_generic_argument : glob_generic_argument -> Sexplib0.Sexp.t
Sourceval glob_generic_argument_of_sexp : Sexplib0.Sexp.t -> glob_generic_argument
Sourceval glob_generic_argument_to_yojson : glob_generic_argument -> Yojson.Safe.t
Sourceval hash_fold_glob_generic_argument : Ppx_hash_lib.Std.Hash.state -> glob_generic_argument -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_glob_generic_argument : glob_generic_argument -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_glob_generic_argument : glob_generic_argument -> glob_generic_argument -> int
Sourcetype raw_generic_argument = Genarg.raw_generic_argument
Sourceval sexp_of_raw_generic_argument : raw_generic_argument -> Sexplib0.Sexp.t
Sourceval raw_generic_argument_of_sexp : Sexplib0.Sexp.t -> raw_generic_argument
Sourceval raw_generic_argument_to_yojson : raw_generic_argument -> Yojson.Safe.t
Sourceval hash_fold_raw_generic_argument : Ppx_hash_lib.Std.Hash.state -> raw_generic_argument -> Ppx_hash_lib.Std.Hash.state
Sourceval hash_raw_generic_argument : raw_generic_argument -> Ppx_hash_lib.Std.Hash.hash_value
Sourceval compare_raw_generic_argument : raw_generic_argument -> raw_generic_argument -> int
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. raw_hash : 'raw Ppx_hash_lib.Std.Hash.folder;
  4. raw_compare : 'raw -> 'raw -> int;
  5. glb_ser : 'glb -> Sexplib.Sexp.t;
  6. glb_des : Sexplib.Sexp.t -> 'glb;
  7. glb_hash : 'glb Ppx_hash_lib.Std.Hash.folder;
  8. glb_compare : 'glb -> 'glb -> int;
  9. top_ser : 'top -> Sexplib.Sexp.t;
  10. top_des : Sexplib.Sexp.t -> 'top;
  11. top_hash : 'top Ppx_hash_lib.Std.Hash.folder;
  12. top_compare : 'top -> 'top -> int;
}
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 Ppx_hash_lib.Std.Hash.folder -> 't Ppx_compare_lib.compare -> ('t, 't, 't) gen_ser
Sourceval mk_vernac_arg : ('t -> Sexplib.Sexp.t) -> (Sexplib.Sexp.t -> 't) -> 't Ppx_hash_lib.Std.Hash.folder -> 't Ppx_compare_lib.compare -> ('t, Util.Empty.t, Util.Empty.t) gen_ser
Sourcemodule type GenSer0 = sig ... end
Sourcemodule GS0 (M : GenSer0) : sig ... end
Sourcemodule GSV (M : GenSer0) : sig ... end
Sourcemodule type GenSer = sig ... end
Sourcemodule GS (M : GenSer) : sig ... end
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