coq-serapi 8.19.0+0.19.0 · OCaml Package

type rlevel = Genarg.rlevel

val rlevel_to_yojson : rlevel -> Yojson.Safe.t

val rlevel_of_yojson : 
  Yojson.Safe.t ->
  rlevel Ppx_deriving_yojson_runtime.error_or

val sexp_of_rlevel : rlevel -> Sexplib0.Sexp.t

val rlevel_of_sexp : Sexplib0.Sexp.t -> rlevel

val hash_fold_rlevel : Base.Hash.state -> rlevel -> Base.Hash.state

val hash_rlevel : rlevel -> Base.Hash.hash_value

val compare_rlevel : rlevel -> rlevel -> int

type glevel = Genarg.glevel

val glevel_to_yojson : glevel -> Yojson.Safe.t

val glevel_of_yojson : 
  Yojson.Safe.t ->
  glevel Ppx_deriving_yojson_runtime.error_or

val sexp_of_glevel : glevel -> Sexplib0.Sexp.t

val glevel_of_sexp : Sexplib0.Sexp.t -> glevel

val hash_fold_glevel : Base.Hash.state -> glevel -> Base.Hash.state

val hash_glevel : glevel -> Base.Hash.hash_value

val compare_glevel : glevel -> glevel -> int

type tlevel = Genarg.tlevel

val tlevel_to_yojson : tlevel -> Yojson.Safe.t

val tlevel_of_yojson : 
  Yojson.Safe.t ->
  tlevel Ppx_deriving_yojson_runtime.error_or

val sexp_of_tlevel : tlevel -> Sexplib0.Sexp.t

val tlevel_of_sexp : Sexplib0.Sexp.t -> tlevel

val hash_fold_tlevel : Base.Hash.state -> tlevel -> Base.Hash.state

val hash_tlevel : tlevel -> Base.Hash.hash_value

val compare_tlevel : tlevel -> tlevel -> int

type 'a generic_argument = 'a Genarg.generic_argument

val generic_argument_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a generic_argument ->
  Yojson.Safe.t

val generic_argument_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a generic_argument Ppx_deriving_yojson_runtime.error_or

val sexp_of_generic_argument : 
  ('a -> Sexplib0.Sexp.t) ->
  'a generic_argument ->
  Sexplib0.Sexp.t

val generic_argument_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a generic_argument

val hash_fold_generic_argument : 
  (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a generic_argument ->
  Base.Hash.state

val compare_generic_argument : 
  ('a -> 'a -> int) ->
  'a generic_argument ->
  'a generic_argument ->
  int

type glob_generic_argument = Genarg.glob_generic_argument

val glob_generic_argument_to_yojson : glob_generic_argument -> Yojson.Safe.t

val glob_generic_argument_of_yojson : 
  Yojson.Safe.t ->
  glob_generic_argument Ppx_deriving_yojson_runtime.error_or

val sexp_of_glob_generic_argument : glob_generic_argument -> Sexplib0.Sexp.t

val glob_generic_argument_of_sexp : Sexplib0.Sexp.t -> glob_generic_argument

val hash_fold_glob_generic_argument : 
  Base.Hash.state ->
  glob_generic_argument ->
  Base.Hash.state

val hash_glob_generic_argument : glob_generic_argument -> Base.Hash.hash_value

val compare_glob_generic_argument : 
  glob_generic_argument ->
  glob_generic_argument ->
  int

type raw_generic_argument = Genarg.raw_generic_argument

val raw_generic_argument_to_yojson : raw_generic_argument -> Yojson.Safe.t

val raw_generic_argument_of_yojson : 
  Yojson.Safe.t ->
  raw_generic_argument Ppx_deriving_yojson_runtime.error_or

val sexp_of_raw_generic_argument : raw_generic_argument -> Sexplib0.Sexp.t

val raw_generic_argument_of_sexp : Sexplib0.Sexp.t -> raw_generic_argument

val hash_fold_raw_generic_argument : 
  Base.Hash.state ->
  raw_generic_argument ->
  Base.Hash.state

val hash_raw_generic_argument : raw_generic_argument -> Base.Hash.hash_value

val compare_raw_generic_argument : 
  raw_generic_argument ->
  raw_generic_argument ->
  int

type typed_generic_argument = Genarg.typed_generic_argument

val typed_generic_argument_of_sexp : 
  Sexplib.Sexp.t ->
  Genarg.typed_generic_argument

val sexp_of_typed_generic_argument : 
  Genarg.typed_generic_argument ->
  Sexplib.Sexp.t

type ('raw, 'glb, 'top) gen_ser = {

raw_ser : 'raw -> Sexplib.Sexp.t;
raw_des : Sexplib.Sexp.t -> 'raw;
raw_hash : 'raw Base.Hash.folder;
raw_compare : 'raw -> 'raw -> int;
glb_ser : 'glb -> Sexplib.Sexp.t;
glb_des : Sexplib.Sexp.t -> 'glb;
glb_hash : 'glb Base.Hash.folder;
glb_compare : 'glb -> 'glb -> int;
top_ser : 'top -> Sexplib.Sexp.t;
top_des : Sexplib.Sexp.t -> 'top;
top_hash : 'top Base.Hash.folder;
top_compare : 'top -> 'top -> int;

}

val register_genser : 
  ('raw, 'glb, 'top) Genarg.genarg_type ->
  ('raw, 'glb, 'top) gen_ser ->
  unit

val gen_ser_pair : 
  ('raw1, 'glb1, 'top1) gen_ser ->
  ('raw2, 'glb2, 'top2) gen_ser ->
  ('raw1 * 'raw2, 'glb1 * 'glb2, 'top1 * 'top2) gen_ser

val gen_ser_list : 
  ('raw, 'glb, 'top) gen_ser ->
  ('raw list, 'glb list, 'top list) gen_ser

val mk_uniform : 
  ('t -> Sexplib.Sexp.t) ->
  (Sexplib.Sexp.t -> 't) ->
  't Base.Hash.folder ->
  't Ppx_compare_lib.compare ->
  ('t, 't, 't) gen_ser

module type GenSer0 = sig ... end

module GS0 (M : GenSer0) : sig ... end

module type GenSer = sig ... end

module GS (M : GenSer) : sig ... end

package coq-serapi