Library v1_mli

Require Import OCaml.OCaml.

Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Module Pervasives.
  Parameter raise : forall {a : Set}, exn -> a.

  Parameter raise_notrace : forall {a : Set}, exn -> a.

  Parameter invalid_arg : forall {a : Set}, string -> a.

  Parameter failwith : forall {a : Set}, string -> a.

  (* exception Exit *)

  Parameter not : bool -> bool.

  Parameter op_andand : bool -> bool -> bool.

  Parameter op_pipepipe : bool -> bool -> bool.

  Parameter __LOC__ : string.

  Parameter __FILE__ : string.

  Parameter __LINE__ : Z.

  Parameter __MODULE__ : string.

  Parameter __POS__ : string * Z * Z * Z.

  Parameter __LOC_OF__ : forall {a : Set}, a -> string * a.

  Parameter __LINE_OF__ : forall {a : Set}, a -> Z * a.

  Parameter __POS_OF__ : forall {a : Set}, a -> (string * Z * Z * Z) * a.

  Parameter op_pipegt : forall {a b : Set}, a -> (a -> b) -> b.

  Parameter op_atat : forall {a b : Set}, (a -> b) -> a -> b.

  Parameter op_tildeminus : Z -> Z.

  Parameter op_tildeplus : Z -> Z.

  Parameter succ : Z -> Z.

  Parameter pred : Z -> Z.

  Parameter op_plus : Z -> Z -> Z.

  Parameter op_minus : Z -> Z -> Z.

  Parameter op_star : Z -> Z -> Z.

  Parameter op_div : Z -> Z -> Z.

  Parameter __mod : Z -> Z -> Z.

  Parameter abs : Z -> Z.

  Parameter max_int : Z.

  Parameter min_int : Z.

  Parameter land : Z -> Z -> Z.

  Parameter lor : Z -> Z -> Z.

  Parameter lxor : Z -> Z -> Z.

  Parameter lnot : Z -> Z.

  Parameter lsl : Z -> Z -> Z.

  Parameter lsr : Z -> Z -> Z.

  Parameter asr : Z -> Z -> Z.

  Parameter op_caret : string -> string -> string.

  Parameter int_of_char : ascii -> Z.

  Parameter char_of_int : Z -> ascii.

  Parameter ignore : forall {a : Set}, a -> unit.

  Parameter string_of_bool : bool -> string.

  Parameter bool_of_string_opt : string -> option bool.

  Parameter string_of_int : Z -> string.

  Parameter int_of_string_opt : string -> option Z.

  Parameter fst : forall {a b : Set}, a * b -> a.

  Parameter snd : forall {a b : Set}, a * b -> b.

  Parameter op_at : forall {a : Set}, list a -> list a -> list a.

  Module ref.
    Record record {a : Set} := {
      contents : a }.
    Arguments record : clear implicits.
  End ref.
  Definition ref := ref.record.

  Parameter __ref_value : forall {a : Set}, a -> ref a.

  Parameter op_exclamation : forall {a : Set}, ref a -> a.

  Parameter op_coloneq : forall {a : Set}, ref a -> a -> unit.

  Parameter incr : ref Z -> unit.

  Parameter decr : ref Z -> unit.

  Inductive result (a b : Set) : Set :=
  | Ok : a -> result a b
  | Error : b -> result a b.

  Arguments Ok {_ _}.
  Arguments Error {_ _}.

  Definition format6 (a b c d e f : Set) :=
    CamlinternalFormatBasics.format6 a b c d e f.

  Definition format4 (a b c d : Set) := format6 a b c c c d.

  Definition format (a b c : Set) := format4 a b c c.

  Parameter string_of_format : forall {a b c d e f : Set},
    format6 a b c d e f -> string.

  Parameter format_of_string : forall {a b c d e f : Set},
    format6 a b c d e f -> format6 a b c d e f.

  Parameter op_caretcaret : forall {a b c d e f g h : Set},
    format6 a b c d e f -> format6 f b c e g h -> format6 a b c d g h.
End Pervasives.

Module List.
  Parameter length : forall {a : Set}, list a -> Z.

  Parameter compare_lengths : forall {a b : Set}, list a -> list b -> Z.

  Parameter compare_length_with : forall {a : Set}, list a -> Z -> Z.

  Parameter cons : forall {a : Set}, a -> list a -> list a.

  Parameter hd : forall {a : Set}, list a -> a.

  Parameter tl : forall {a : Set}, list a -> list a.

  Parameter nth_opt : forall {a : Set}, list a -> Z -> option a.

  Parameter rev : forall {a : Set}, list a -> list a.

  Parameter init : forall {a : Set}, Z -> (Z -> a) -> list a.

  Parameter append : forall {a : Set}, list a -> list a -> list a.

  Parameter rev_append : forall {a : Set}, list a -> list a -> list a.

  Parameter concat : forall {a : Set}, list (list a) -> list a.

  Parameter flatten : forall {a : Set}, list (list a) -> list a.

  Parameter iter : forall {a : Set}, (a -> unit) -> list a -> unit.

  Parameter iteri : forall {a : Set}, (Z -> a -> unit) -> list a -> unit.

  Parameter map : forall {a b : Set}, (a -> b) -> list a -> list b.

  Parameter mapi : forall {a b : Set}, (Z -> a -> b) -> list a -> list b.

  Parameter rev_map : forall {a b : Set}, (a -> b) -> list a -> list b.

  Parameter fold_left : forall {a b : Set}, (a -> b -> a) -> a -> list b -> a.

  Parameter fold_right : forall {a b : Set}, (a -> b -> b) -> list a -> b -> b.

  Parameter iter2 : forall {a b : Set},
    (a -> b -> unit) -> list a -> list b -> unit.

  Parameter map2 : forall {a b c : Set},
    (a -> b -> c) -> list a -> list b -> list c.

  Parameter rev_map2 : forall {a b c : Set},
    (a -> b -> c) -> list a -> list b -> list c.

  Parameter fold_left2 : forall {a b c : Set},
    (a -> b -> c -> a) -> a -> list b -> list c -> a.

  Parameter fold_right2 : forall {a b c : Set},
    (a -> b -> c -> c) -> list a -> list b -> c -> c.

  Parameter for_all : forall {a : Set}, (a -> bool) -> list a -> bool.

  Parameter __exists : forall {a : Set}, (a -> bool) -> list a -> bool.

  Parameter for_all2 : forall {a b : Set},
    (a -> b -> bool) -> list a -> list b -> bool.

  Parameter __exists2 : forall {a b : Set},
    (a -> b -> bool) -> list a -> list b -> bool.

  Parameter mem : forall {a : Set}, a -> list a -> bool.

  Parameter memq : forall {a : Set}, a -> list a -> bool.

  Parameter find_opt : forall {a : Set}, (a -> bool) -> list a -> option a.

  Parameter filter : forall {a : Set}, (a -> bool) -> list a -> list a.

  Parameter find_all : forall {a : Set}, (a -> bool) -> list a -> list a.

  Parameter partition : forall {a : Set},
    (a -> bool) -> list a -> list a * list a.

  Parameter assoc_opt : forall {a b : Set}, a -> list (a * b) -> option b.

  Parameter assq_opt : forall {a b : Set}, a -> list (a * b) -> option b.

  Parameter mem_assoc : forall {a b : Set}, a -> list (a * b) -> bool.

  Parameter mem_assq : forall {a b : Set}, a -> list (a * b) -> bool.

  Parameter remove_assoc : forall {a b : Set},
    a -> list (a * b) -> list (a * b).

  Parameter remove_assq : forall {a b : Set}, a -> list (a * b) -> list (a * b).

  Parameter split : forall {a b : Set}, list (a * b) -> list a * list b.

  Parameter combine : forall {a b : Set}, list a -> list b -> list (a * b).

  Parameter sort : forall {a : Set}, (a -> a -> Z) -> list a -> list a.

  Parameter stable_sort : forall {a : Set}, (a -> a -> Z) -> list a -> list a.

  Parameter fast_sort : forall {a : Set}, (a -> a -> Z) -> list a -> list a.

  Parameter sort_uniq : forall {a : Set}, (a -> a -> Z) -> list a -> list a.

  Parameter merge : forall {a : Set},
    (a -> a -> Z) -> list a -> list a -> list a.
End List.

Module String.
  Parameter length : string -> Z.

  Parameter get : string -> Z -> ascii.

  Parameter make : Z -> ascii -> string.

  Parameter init : Z -> (Z -> ascii) -> string.

  Parameter sub : string -> Z -> Z -> string.

  Parameter blit : string -> Z -> string -> Z -> Z -> unit.

  Parameter concat : string -> list string -> string.

  Parameter iter : (ascii -> unit) -> string -> unit.

  Parameter iteri : (Z -> ascii -> unit) -> string -> unit.

  Parameter map : (ascii -> ascii) -> string -> string.

  Parameter mapi : (Z -> ascii -> ascii) -> string -> string.

  Parameter trim : string -> string.

  Parameter escaped : string -> string.

  Parameter index_opt : string -> ascii -> option Z.

  Parameter rindex_opt : string -> ascii -> option Z.

  Parameter index_from_opt : string -> Z -> ascii -> option Z.

  Parameter rindex_from_opt : string -> Z -> ascii -> option Z.

  Parameter contains : string -> ascii -> bool.

  Parameter contains_from : string -> Z -> ascii -> bool.

  Parameter rcontains_from : string -> Z -> ascii -> bool.

  Parameter uppercase_ascii : string -> string.

  Parameter lowercase_ascii : string -> string.

  Parameter capitalize_ascii : string -> string.

  Parameter uncapitalize_ascii : string -> string.

  Definition t := string.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter split_on_char : ascii -> string -> list string.

  Parameter get_char : t -> Z -> ascii.

  Parameter get_uint8 : t -> Z -> Z.

  Parameter get_int8 : t -> Z -> Z.

  Parameter get_uint16 : t -> Z -> Z.

  Parameter get_int16 : t -> Z -> Z.

  Parameter get_int32 : t -> Z -> int32.

  Parameter get_int64 : t -> Z -> int64.

  Module LE.
    Parameter get_uint16 : t -> Z -> Z.

    Parameter get_int16 : t -> Z -> Z.

    Parameter get_int32 : t -> Z -> int32.

    Parameter get_int64 : t -> Z -> int64.
  End LE.
End String.

Module Int32.
  Parameter zero : int32.

  Parameter one : int32.

  Parameter minus_one : int32.

  Parameter neg : int32 -> int32.

  Parameter add : int32 -> int32 -> int32.

  Parameter sub : int32 -> int32 -> int32.

  Parameter mul : int32 -> int32 -> int32.

  Parameter div : int32 -> int32 -> int32.

  Parameter rem : int32 -> int32 -> int32.

  Parameter succ : int32 -> int32.

  Parameter pred : int32 -> int32.

  Parameter abs : int32 -> int32.

  Parameter max_int : int32.

  Parameter min_int : int32.

  Parameter logand : int32 -> int32 -> int32.

  Parameter logor : int32 -> int32 -> int32.

  Parameter logxor : int32 -> int32 -> int32.

  Parameter lognot : int32 -> int32.

  Parameter shift_left : int32 -> Z -> int32.

  Parameter shift_right : int32 -> Z -> int32.

  Parameter shift_right_logical : int32 -> Z -> int32.

  Parameter of_int : Z -> int32.

  Parameter to_int : int32 -> Z.

  Parameter of_float : Z -> int32.

  Parameter to_float : int32 -> Z.

  Parameter of_string : string -> int32.

  Parameter of_string_opt : string -> option int32.

  Parameter to_string : int32 -> string.

  Parameter bits_of_float : Z -> int32.

  Parameter float_of_bits : int32 -> Z.

  Definition t := int32.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.
End Int32.

Module Int64.
  Parameter zero : int64.

  Parameter one : int64.

  Parameter minus_one : int64.

  Parameter neg : int64 -> int64.

  Parameter add : int64 -> int64 -> int64.

  Parameter sub : int64 -> int64 -> int64.

  Parameter mul : int64 -> int64 -> int64.

  Parameter div : int64 -> int64 -> int64.

  Parameter rem : int64 -> int64 -> int64.

  Parameter succ : int64 -> int64.

  Parameter pred : int64 -> int64.

  Parameter abs : int64 -> int64.

  Parameter max_int : int64.

  Parameter min_int : int64.

  Parameter logand : int64 -> int64 -> int64.

  Parameter logor : int64 -> int64 -> int64.

  Parameter logxor : int64 -> int64 -> int64.

  Parameter lognot : int64 -> int64.

  Parameter shift_left : int64 -> Z -> int64.

  Parameter shift_right : int64 -> Z -> int64.

  Parameter shift_right_logical : int64 -> Z -> int64.

  Parameter of_int : Z -> int64.

  Parameter to_int : int64 -> Z.

  Parameter of_float : Z -> int64.

  Parameter to_float : int64 -> Z.

  Parameter of_int32 : int32 -> int64.

  Parameter to_int32 : int64 -> int32.

  Parameter of_nativeint : nativeint -> int64.

  Parameter to_nativeint : int64 -> nativeint.

  Parameter of_string : string -> int64.

  Parameter of_string_opt : string -> option int64.

  Parameter to_string : int64 -> string.

  Parameter bits_of_float : Z -> int64.

  Parameter float_of_bits : int64 -> Z.

  Definition t := int64.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.
End Int64.

Module Format.
  Parameter formatter : Set.

  Parameter pp_open_box : formatter -> Z -> unit.

  Parameter pp_close_box : formatter -> unit -> unit.

  Parameter pp_open_hbox : formatter -> unit -> unit.

  Parameter pp_open_vbox : formatter -> Z -> unit.

  Parameter pp_open_hvbox : formatter -> Z -> unit.

  Parameter pp_open_hovbox : formatter -> Z -> unit.

  Parameter pp_print_string : formatter -> string -> unit.

  Parameter pp_print_as : formatter -> Z -> string -> unit.

  Parameter pp_print_int : formatter -> Z -> unit.

  Parameter pp_print_float : formatter -> Z -> unit.

  Parameter pp_print_char : formatter -> ascii -> unit.

  Parameter pp_print_bool : formatter -> bool -> unit.

  Parameter pp_print_space : formatter -> unit -> unit.

  Parameter pp_print_cut : formatter -> unit -> unit.

  Parameter pp_print_break : formatter -> Z -> Z -> unit.

  Parameter pp_force_newline : formatter -> unit -> unit.

  Parameter pp_print_if_newline : formatter -> unit -> unit.

  Parameter pp_print_flush : formatter -> unit -> unit.

  Parameter pp_print_newline : formatter -> unit -> unit.

  Parameter pp_set_margin : formatter -> Z -> unit.

  Parameter pp_get_margin : formatter -> unit -> Z.

  Parameter pp_set_max_indent : formatter -> Z -> unit.

  Parameter pp_get_max_indent : formatter -> unit -> Z.

  Parameter pp_set_max_boxes : formatter -> Z -> unit.

  Parameter pp_get_max_boxes : formatter -> unit -> Z.

  Parameter pp_over_max_boxes : formatter -> unit -> bool.

  Parameter pp_open_tbox : formatter -> unit -> unit.

  Parameter pp_close_tbox : formatter -> unit -> unit.

  Parameter pp_set_tab : formatter -> unit -> unit.

  Parameter pp_print_tab : formatter -> unit -> unit.

  Parameter pp_print_tbreak : formatter -> Z -> Z -> unit.

  Parameter pp_set_ellipsis_text : formatter -> string -> unit.

  Parameter pp_get_ellipsis_text : formatter -> unit -> string.

  Definition tag := string.

  Parameter pp_open_tag : formatter -> string -> unit.

  Parameter pp_close_tag : formatter -> unit -> unit.

  Parameter pp_set_tags : formatter -> bool -> unit.

  Parameter pp_set_print_tags : formatter -> bool -> unit.

  Parameter pp_set_mark_tags : formatter -> bool -> unit.

  Parameter pp_get_print_tags : formatter -> unit -> bool.

  Parameter pp_get_mark_tags : formatter -> unit -> bool.

  Parameter pp_print_list : forall {a : Set},
    option (formatter -> unit -> unit) -> (formatter -> a -> unit) ->
    formatter -> list a -> unit.

  Parameter pp_print_text : formatter -> string -> unit.

  Parameter fprintf : forall {a : Set},
    formatter -> Pervasives.format a formatter unit -> a.

  Parameter sprintf : forall {a : Set}, Pervasives.format a unit string -> a.

  Parameter asprintf : forall {a : Set},
    Pervasives.format4 a formatter unit string -> a.

  Parameter ifprintf : forall {a : Set},
    formatter -> Pervasives.format a formatter unit -> a.

  Parameter kfprintf : forall {a b : Set},
    (formatter -> a) -> formatter -> Pervasives.format4 b formatter unit a -> b.

  Parameter ikfprintf : forall {a b : Set},
    (formatter -> a) -> formatter -> Pervasives.format4 b formatter unit a -> b.

  Parameter ksprintf : forall {a b : Set},
    (string -> a) -> Pervasives.format4 b unit string a -> b.

  Parameter kasprintf : forall {a b : Set},
    (string -> a) -> Pervasives.format4 b formatter unit a -> b.
End Format.

Module MBytes.
  Parameter t : Set.

  Parameter create : Z -> t.

  Parameter length : t -> Z.

  Parameter copy : t -> t.

  Parameter sub : t -> Z -> Z -> t.

  Parameter blit : t -> Z -> t -> Z -> Z -> unit.

  Parameter blit_of_string : string -> Z -> t -> Z -> Z -> unit.

  Parameter blit_to_bytes : t -> Z -> string -> Z -> Z -> unit.

  Parameter of_string : string -> t.

  Parameter to_string : t -> string.

  Parameter sub_string : t -> Z -> Z -> string.

  Parameter get_char : t -> Z -> ascii.

  Parameter get_uint8 : t -> Z -> Z.

  Parameter get_int8 : t -> Z -> Z.

  Parameter set_char : t -> Z -> ascii -> unit.

  Parameter set_int8 : t -> Z -> Z -> unit.

  Parameter get_uint16 : t -> Z -> Z.

  Parameter get_int16 : t -> Z -> Z.

  Parameter get_int32 : t -> Z -> int32.

  Parameter get_int64 : t -> Z -> int64.

  Parameter set_int16 : t -> Z -> Z -> unit.

  Parameter set_int32 : t -> Z -> int32 -> unit.

  Parameter set_int64 : t -> Z -> int64 -> unit.

  Module LE.
    Parameter get_uint16 : t -> Z -> Z.

    Parameter get_int16 : t -> Z -> Z.

    Parameter get_int32 : t -> Z -> int32.

    Parameter get_int64 : t -> Z -> int64.

    Parameter set_int16 : t -> Z -> Z -> unit.

    Parameter set_int32 : t -> Z -> int32 -> unit.

    Parameter set_int64 : t -> Z -> int64 -> unit.
  End LE.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter concat : string -> list t -> t.

  Parameter to_hex : t -> (* `Hex *) string.

  Parameter of_hex : (* `Hex *) string -> t.
End MBytes.

Module Z.
  Parameter t : Set.

  Parameter zero : t.

  Parameter one : t.

  Parameter succ : t -> t.

  Parameter abs : t -> t.

  Parameter neg : t -> t.

  Parameter add : t -> t -> t.

  Parameter sub : t -> t -> t.

  Parameter mul : t -> t -> t.

  Parameter ediv_rem : t -> t -> t * t.

  Parameter logand : t -> t -> t.

  Parameter logor : t -> t -> t.

  Parameter logxor : t -> t -> t.

  Parameter lognot : t -> t.

  Parameter shift_left : t -> Z -> t.

  Parameter shift_right : t -> Z -> t.

  Parameter to_string : t -> string.

  Parameter of_string : string -> t.

  Parameter to_int64 : t -> int64.

  Parameter of_int64 : int64 -> t.

  Parameter to_int : t -> Z.

  Parameter of_int : Z -> t.

  Parameter to_bits : option Z -> t -> MBytes.t.

  Parameter of_bits : MBytes.t -> t.

  Parameter equal : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter numbits : t -> Z.
End Z.

Module Lwt.
  Parameter t : forall (a : Set), Set.

  Parameter __return : forall {a : Set}, a -> t a.

  Parameter bind : forall {a b : Set}, t a -> (a -> t b) -> t b.

  Parameter op_gtgteq : forall {a b : Set}, t a -> (a -> t b) -> t b.

  Parameter op_eqltlt : forall {a b : Set}, (a -> t b) -> t a -> t b.

  Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

  Parameter op_gtpipeeq : forall {a b : Set}, t a -> (a -> b) -> t b.

  Parameter op_eqpipelt : forall {a b : Set}, (a -> b) -> t a -> t b.

  Parameter return_unit : t unit.

  Parameter return_none : forall {a : Set}, t (option a).

  Parameter return_nil : forall {a : Set}, t (list a).

  Parameter return_true : t bool.

  Parameter return_false : t bool.

  Parameter join : list (t unit) -> t unit.

  Parameter op_ltandgt : t unit -> t unit -> t unit.
End Lwt.

Module Lwt_list.
  Parameter map_s : forall {a b : Set},
    (a -> Lwt.t b) -> list a -> Lwt.t (list b).

  Parameter map_p : forall {a b : Set},
    (a -> Lwt.t b) -> list a -> Lwt.t (list b).

  Parameter mapi_s : forall {a b : Set},
    (Z -> a -> Lwt.t b) -> list a -> Lwt.t (list b).

  Parameter mapi_p : forall {a b : Set},
    (Z -> a -> Lwt.t b) -> list a -> Lwt.t (list b).

  Parameter rev_map_s : forall {a b : Set},
    (a -> Lwt.t b) -> list a -> Lwt.t (list b).

  Parameter rev_map_p : forall {a b : Set},
    (a -> Lwt.t b) -> list a -> Lwt.t (list b).

  Parameter fold_left_s : forall {a b : Set},
    (a -> b -> Lwt.t a) -> a -> list b -> Lwt.t a.

  Parameter fold_right_s : forall {a b : Set},
    (a -> b -> Lwt.t b) -> list a -> b -> Lwt.t b.

  Parameter for_all_s : forall {a : Set},
    (a -> Lwt.t bool) -> list a -> Lwt.t bool.

  Parameter for_all_p : forall {a : Set},
    (a -> Lwt.t bool) -> list a -> Lwt.t bool.

  Parameter exists_s : forall {a : Set},
    (a -> Lwt.t bool) -> list a -> Lwt.t bool.

  Parameter exists_p : forall {a : Set},
    (a -> Lwt.t bool) -> list a -> Lwt.t bool.

  Parameter find_s : forall {a : Set}, (a -> Lwt.t bool) -> list a -> Lwt.t a.

  Parameter filter_s : forall {a : Set},
    (a -> Lwt.t bool) -> list a -> Lwt.t (list a).

  Parameter filter_p : forall {a : Set},
    (a -> Lwt.t bool) -> list a -> Lwt.t (list a).

  Parameter filter_map_s : forall {a b : Set},
    (a -> Lwt.t (option b)) -> list a -> Lwt.t (list b).

  Parameter filter_map_p : forall {a b : Set},
    (a -> Lwt.t (option b)) -> list a -> Lwt.t (list b).

  Parameter partition_s : forall {a : Set},
    (a -> Lwt.t bool) -> list a -> Lwt.t (list a * list a).

  Parameter partition_p : forall {a : Set},
    (a -> Lwt.t bool) -> list a -> Lwt.t (list a * list a).
End Lwt_list.

Module Raw_hashes.
  Parameter blake2b : MBytes.t -> MBytes.t.

  Parameter sha256 : MBytes.t -> MBytes.t.

  Parameter sha512 : MBytes.t -> MBytes.t.
End Raw_hashes.

Module Compare.
  Module COMPARABLE.
    Record signature {t : Set} := {
      t := t;
      compare : t -> t -> Z;
    }.
    Arguments signature : clear implicits.
  End COMPARABLE.

  Module S.
    Record signature {t : Set} := {
      t := t;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
    }.
    Arguments signature : clear implicits.
  End S.

  Module Make.
    (* Unhandled functor *)
  End Make.

  Module Char.
    Definition t := ascii.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Char.

  Module Bool.
    Definition t := bool.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Bool.

  Module Int.
    Definition t := Z.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Int.

  Module Int32.
    Definition t := int32.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Int32.

  Module Uint32.
    Definition t := int32.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Uint32.

  Module Int64.
    Definition t := int64.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Int64.

  Module Uint64.
    Definition t := int64.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Uint64.

  Module Float.
    Definition t := Z.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Float.

  Module String.
    Definition t := string.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End String.

  Module Z.
    Definition t := Z.t.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.
  End Z.

  Module List.
    (* Unhandled functor *)
  End List.

  Module Option.
    (* Unhandled functor *)
  End Option.
End Compare.

Module Data_encoding.
  Inductive json : Set :=
  | Bool : bool -> json
  | Null : json
  | O : list (string * json) -> json
  | Float : Z -> json
  | String : string -> json
  | A : list json -> json.

  Parameter json_schema : Set.

  Parameter t : forall (a : Set), Set.

  Definition encoding (a : Set) := t a.

  Parameter classify : forall {a : Set},
    encoding a -> (* `Variable *) unit + (* `Fixed *) Z + (* `Dynamic *) unit.

  Parameter splitted : forall {a : Set}, encoding a -> encoding a -> encoding a.

  Parameter null : encoding unit.

  Parameter empty : encoding unit.

  Parameter __unit_value : encoding unit.

  Parameter constant : string -> encoding unit.

  Parameter int8 : encoding Z.

  Parameter uint8 : encoding Z.

  Parameter int16 : encoding Z.

  Parameter uint16 : encoding Z.

  Parameter int31 : encoding Z.

  Parameter __int32_value : encoding int32.

  Parameter __int64_value : encoding int64.

  Parameter n : encoding Z.t.

  Parameter z : encoding Z.t.

  Parameter __bool_value : encoding bool.

  Parameter __string_value : encoding string.

  Parameter __bytes_value : encoding MBytes.t.

  Parameter __float_value : encoding Z.

  Parameter __option_value : forall {a : Set},
    encoding a -> encoding (option a).

  Parameter string_enum : forall {a : Set}, list (string * a) -> encoding a.

  Module Fixed.
    Parameter __string_value : Z -> encoding string.

    Parameter __bytes_value : Z -> encoding MBytes.t.

    Parameter add_padding : forall {a : Set}, encoding a -> Z -> encoding a.
  End Fixed.

  Module __Variable.
    Parameter __string_value : encoding string.

    Parameter __bytes_value : encoding MBytes.t.

    Parameter array : forall {a : Set},
      option Z -> encoding a -> encoding (array a).

    Parameter __list_value : forall {a : Set},
      option Z -> encoding a -> encoding (list a).
  End __Variable.

  Module Bounded.
    Parameter __string_value : Z -> encoding string.

    Parameter __bytes_value : Z -> encoding MBytes.t.
  End Bounded.

  Parameter dynamic_size : forall {a : Set},
    option ((* `Uint16 *) unit + (* `Uint8 *) unit + (* `Uint30 *) unit) ->
    encoding a -> encoding a.

  Parameter __json_value : encoding json.

  Parameter __json_schema_value : encoding json_schema.

  Parameter field : forall (a : Set), Set.

  Parameter req : forall {t : Set},
    option string -> option string -> string -> encoding t -> field t.

  Parameter opt : forall {t : Set},
    option string -> option string -> string -> encoding t -> field (option t).

  Parameter varopt : forall {t : Set},
    option string -> option string -> string -> encoding t -> field (option t).

  Parameter dft : forall {t : Set},
    option string -> option string -> string -> encoding t -> t -> field t.

  Parameter obj1 : forall {f1 : Set}, field f1 -> encoding f1.

  Parameter obj2 : forall {f1 f2 : Set},
    field f1 -> field f2 -> encoding (f1 * f2).

  Parameter obj3 : forall {f1 f2 f3 : Set},
    field f1 -> field f2 -> field f3 -> encoding (f1 * f2 * f3).

  Parameter obj4 : forall {f1 f2 f3 f4 : Set},
    field f1 -> field f2 -> field f3 -> field f4 -> encoding (f1 * f2 * f3 * f4).

  Parameter obj5 : forall {f1 f2 f3 f4 f5 : Set},
    field f1 -> field f2 -> field f3 -> field f4 -> field f5 ->
    encoding (f1 * f2 * f3 * f4 * f5).

  Parameter obj6 : forall {f1 f2 f3 f4 f5 f6 : Set},
    field f1 -> field f2 -> field f3 -> field f4 -> field f5 -> field f6 ->
    encoding (f1 * f2 * f3 * f4 * f5 * f6).

  Parameter obj7 : forall {f1 f2 f3 f4 f5 f6 f7 : Set},
    field f1 -> field f2 -> field f3 -> field f4 -> field f5 -> field f6 ->
    field f7 -> encoding (f1 * f2 * f3 * f4 * f5 * f6 * f7).

  Parameter obj8 : forall {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
    field f1 -> field f2 -> field f3 -> field f4 -> field f5 -> field f6 ->
    field f7 -> field f8 -> encoding (f1 * f2 * f3 * f4 * f5 * f6 * f7 * f8).

  Parameter obj9 : forall {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    field f1 -> field f2 -> field f3 -> field f4 -> field f5 -> field f6 ->
    field f7 -> field f8 -> field f9 ->
    encoding (f1 * f2 * f3 * f4 * f5 * f6 * f7 * f8 * f9).

  Parameter obj10 : forall {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    field f1 -> field f2 -> field f3 -> field f4 -> field f5 -> field f6 ->
    field f7 -> field f8 -> field f9 -> field f10 ->
    encoding (f1 * f2 * f3 * f4 * f5 * f6 * f7 * f8 * f9 * f10).

  Parameter tup1 : forall {f1 : Set}, encoding f1 -> encoding f1.

  Parameter tup2 : forall {f1 f2 : Set},
    encoding f1 -> encoding f2 -> encoding (f1 * f2).

  Parameter tup3 : forall {f1 f2 f3 : Set},
    encoding f1 -> encoding f2 -> encoding f3 -> encoding (f1 * f2 * f3).

  Parameter tup4 : forall {f1 f2 f3 f4 : Set},
    encoding f1 -> encoding f2 -> encoding f3 -> encoding f4 ->
    encoding (f1 * f2 * f3 * f4).

  Parameter tup5 : forall {f1 f2 f3 f4 f5 : Set},
    encoding f1 -> encoding f2 -> encoding f3 -> encoding f4 -> encoding f5 ->
    encoding (f1 * f2 * f3 * f4 * f5).

  Parameter tup6 : forall {f1 f2 f3 f4 f5 f6 : Set},
    encoding f1 -> encoding f2 -> encoding f3 -> encoding f4 -> encoding f5 ->
    encoding f6 -> encoding (f1 * f2 * f3 * f4 * f5 * f6).

  Parameter tup7 : forall {f1 f2 f3 f4 f5 f6 f7 : Set},
    encoding f1 -> encoding f2 -> encoding f3 -> encoding f4 -> encoding f5 ->
    encoding f6 -> encoding f7 -> encoding (f1 * f2 * f3 * f4 * f5 * f6 * f7).

  Parameter tup8 : forall {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
    encoding f1 -> encoding f2 -> encoding f3 -> encoding f4 -> encoding f5 ->
    encoding f6 -> encoding f7 -> encoding f8 ->
    encoding (f1 * f2 * f3 * f4 * f5 * f6 * f7 * f8).

  Parameter tup9 : forall {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    encoding f1 -> encoding f2 -> encoding f3 -> encoding f4 -> encoding f5 ->
    encoding f6 -> encoding f7 -> encoding f8 -> encoding f9 ->
    encoding (f1 * f2 * f3 * f4 * f5 * f6 * f7 * f8 * f9).

  Parameter tup10 : forall {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
    encoding f1 -> encoding f2 -> encoding f3 -> encoding f4 -> encoding f5 ->
    encoding f6 -> encoding f7 -> encoding f8 -> encoding f9 -> encoding f10 ->
    encoding (f1 * f2 * f3 * f4 * f5 * f6 * f7 * f8 * f9 * f10).

  Parameter merge_objs : forall {o1 o2 : Set},
    encoding o1 -> encoding o2 -> encoding (o1 * o2).

  Parameter merge_tups : forall {a1 a2 : Set},
    encoding a1 -> encoding a2 -> encoding (a1 * a2).

  Parameter array : forall {a : Set},
    option Z -> encoding a -> encoding (array a).

  Parameter __list_value : forall {a : Set},
    option Z -> encoding a -> encoding (list a).

  Parameter assoc : forall {a : Set},
    encoding a -> encoding (list (string * a)).

  Inductive case_tag : Set :=
  | Tag : Z -> case_tag
  | Json_only : case_tag.

  Parameter case : forall (t : Set), Set.

  Parameter __case_value : forall {a t : Set},
    string -> option string -> case_tag -> encoding a -> (t -> option a) ->
    (a -> t) -> case t.

  Parameter union : forall {t : Set},
    option ((* `Uint16 *) unit + (* `Uint8 *) unit) -> list (case t) ->
    encoding t.

  Parameter def : forall {t : Set},
    string -> option string -> option string -> encoding t -> encoding t.

  Parameter conv : forall {a b : Set},
    (a -> b) -> (b -> a) -> option json_schema -> encoding b -> encoding a.

  Parameter mu : forall {a : Set},
    string -> option string -> option string -> (encoding a -> encoding a) ->
    encoding a.

  Parameter lazy_t : forall (a : Set), Set.

  Parameter lazy_encoding : forall {a : Set}, encoding a -> encoding (lazy_t a).

  Parameter force_decode : forall {a : Set}, lazy_t a -> option a.

  Parameter force_bytes : forall {a : Set}, lazy_t a -> MBytes.t.

  Parameter make_lazy : forall {a : Set}, encoding a -> a -> lazy_t a.

  Parameter apply_lazy : forall {a b : Set},
    (a -> b) -> (MBytes.t -> b) -> (b -> b -> b) -> lazy_t a -> b.

  Module Json.
    Parameter schema : forall {a : Set},
      option string -> encoding a -> json_schema.

    Parameter construct : forall {t : Set}, encoding t -> t -> json.

    Parameter destruct : forall {t : Set}, encoding t -> json -> t.

    Reserved Notation "'path".

    Inductive path_item : Set :=
    | Index : Z -> path_item
    | Field : string -> path_item
    | Next : path_item
    | Star : path_item
    
    where "'path" := (list path_item).

    Definition path := 'path.

    (* exception Cannot_destruct *)

    (* exception Unexpected *)

    (* exception No_case_matched *)

    (* exception Bad_array_size *)

    (* exception Missing_field *)

    (* exception Unexpected_field *)

    Parameter print_error :
      option (Format.formatter -> exn -> unit) -> Format.formatter -> exn ->
      unit.

    Parameter cannot_destruct : forall {a b : Set},
      Pervasives.format4 a Format.formatter unit b -> a.

    Parameter wrap_error : forall {a b : Set}, (a -> b) -> a -> b.

    Parameter pp : Format.formatter -> json -> unit.
  End Json.

  Module Binary.
    Parameter length : forall {a : Set}, encoding a -> a -> Z.

    Parameter fixed_length : forall {a : Set}, encoding a -> option Z.

    Parameter read : forall {a : Set},
      encoding a -> MBytes.t -> Z -> Z -> option (Z * a).

    Parameter write : forall {a : Set},
      encoding a -> a -> MBytes.t -> Z -> Z -> option Z.

    Parameter to_bytes : forall {a : Set}, encoding a -> a -> option MBytes.t.

    Parameter to_bytes_exn : forall {a : Set}, encoding a -> a -> MBytes.t.

    Parameter of_bytes : forall {a : Set}, encoding a -> MBytes.t -> option a.

    Parameter write_error : Set.

    (* exception Write_error *)
  End Binary.

  Parameter check_size : forall {a : Set}, Z -> encoding a -> encoding a.
End Data_encoding.

Module Error_monad.
  Inductive error_category : Set :=
  | Permanent : error_category
  | Temporary : error_category
  | Branch : error_category.

  Definition __error := extensible_type.

  Parameter pp : Format.formatter -> __error -> unit.

  Parameter error_encoding : Data_encoding.t __error.

  Parameter json_of_error : __error -> Data_encoding.json.

  Parameter error_of_json : Data_encoding.json -> __error.

  Module error_info.
    Record record := {
      category : error_category;
      id : string;
      title : string;
      description : string;
      schema : Data_encoding.json_schema }.
  End error_info.
  Definition error_info := error_info.record.

  Parameter pp_info : Format.formatter -> error_info -> unit.

  Parameter get_registered_errors : unit -> list error_info.

  Parameter register_error_kind : forall {err : Set},
    error_category -> string -> string -> string ->
    option (Format.formatter -> err -> unit) -> Data_encoding.t err ->
    (__error -> option err) -> (err -> __error) -> unit.

  Parameter classify_errors : list __error -> error_category.

  Definition tzresult (a : Set) := Pervasives.result a (list __error).

  Parameter result_encoding : forall {a : Set},
    Data_encoding.t a -> Data_encoding.encoding (tzresult a).

  Parameter ok : forall {a : Set}, a -> tzresult a.

  Parameter __return : forall {a : Set}, a -> Lwt.t (tzresult a).

  Parameter return_unit : Lwt.t (tzresult unit).

  Parameter return_none : forall {a : Set}, Lwt.t (tzresult (option a)).

  Parameter return_some : forall {a : Set}, a -> Lwt.t (tzresult (option a)).

  Parameter return_nil : forall {a : Set}, Lwt.t (tzresult (list a)).

  Parameter return_true : Lwt.t (tzresult bool).

  Parameter return_false : Lwt.t (tzresult bool).

  Parameter __error_value : forall {a : Set}, __error -> tzresult a.

  Parameter fail : forall {a : Set}, __error -> Lwt.t (tzresult a).

  Parameter op_gtgtquestion : forall {a b : Set},
    tzresult a -> (a -> tzresult b) -> tzresult b.

  Parameter op_gtgteqquestion : forall {a b : Set},
    Lwt.t (tzresult a) -> (a -> Lwt.t (tzresult b)) -> Lwt.t (tzresult b).

  Parameter op_gtgteq : forall {a b : Set},
    Lwt.t a -> (a -> Lwt.t b) -> Lwt.t b.

  Parameter op_gtpipeeq : forall {a b : Set}, Lwt.t a -> (a -> b) -> Lwt.t b.

  Parameter op_gtgtpipequestion : forall {a b : Set},
    Lwt.t (tzresult a) -> (a -> b) -> Lwt.t (tzresult b).

  Parameter op_gtpipequestion : forall {a b : Set},
    tzresult a -> (a -> b) -> tzresult b.

  Parameter record_trace : forall {a : Set},
    __error -> tzresult a -> tzresult a.

  Parameter trace : forall {b : Set},
    __error -> Lwt.t (tzresult b) -> Lwt.t (tzresult b).

  Parameter record_trace_eval : forall {a : Set},
    (unit -> tzresult __error) -> tzresult a -> tzresult a.

  Parameter trace_eval : forall {b : Set},
    (unit -> Lwt.t (tzresult __error)) -> Lwt.t (tzresult b) ->
    Lwt.t (tzresult b).

  Parameter fail_unless : bool -> __error -> Lwt.t (tzresult unit).

  Parameter fail_when : bool -> __error -> Lwt.t (tzresult unit).

  Parameter iter_s : forall {a : Set},
    (a -> Lwt.t (tzresult unit)) -> list a -> Lwt.t (tzresult unit).

  Parameter iter_p : forall {a : Set},
    (a -> Lwt.t (tzresult unit)) -> list a -> Lwt.t (tzresult unit).

  Parameter map_s : forall {a b : Set},
    (a -> Lwt.t (tzresult b)) -> list a -> Lwt.t (tzresult (list b)).

  Parameter map_p : forall {a b : Set},
    (a -> Lwt.t (tzresult b)) -> list a -> Lwt.t (tzresult (list b)).

  Parameter map2 : forall {a b c : Set},
    (a -> b -> tzresult c) -> list a -> list b -> tzresult (list c).

  Parameter map2_s : forall {a b c : Set},
    (a -> b -> Lwt.t (tzresult c)) -> list a -> list b ->
    Lwt.t (tzresult (list c)).

  Parameter filter_map_s : forall {a b : Set},
    (a -> Lwt.t (tzresult (option b))) -> list a -> Lwt.t (tzresult (list b)).

  Parameter fold_left_s : forall {a b : Set},
    (a -> b -> Lwt.t (tzresult a)) -> a -> list b -> Lwt.t (tzresult a).

  Parameter fold_right_s : forall {a b : Set},
    (a -> b -> Lwt.t (tzresult b)) -> list a -> b -> Lwt.t (tzresult b).

  Parameter shell_error : Set.

  Definition shell_tzresult (a : Set) := Pervasives.result a (list shell_error).
End Error_monad.

Module Logging.
  Parameter debug : forall {a : Set},
    Pervasives.format4 a Format.formatter unit unit -> a.

  Parameter log_info : forall {a : Set},
    Pervasives.format4 a Format.formatter unit unit -> a.

  Parameter log_notice : forall {a : Set},
    Pervasives.format4 a Format.formatter unit unit -> a.

  Parameter warn : forall {a : Set},
    Pervasives.format4 a Format.formatter unit unit -> a.

  Parameter log_error : forall {a : Set},
    Pervasives.format4 a Format.formatter unit unit -> a.

  Parameter fatal_error : forall {a : Set},
    Pervasives.format4 a Format.formatter unit unit -> a.

  Parameter lwt_debug : forall {a : Set},
    Pervasives.format4 a Format.formatter unit (Lwt.t unit) -> a.

  Parameter lwt_log_info : forall {a : Set},
    Pervasives.format4 a Format.formatter unit (Lwt.t unit) -> a.

  Parameter lwt_log_notice : forall {a : Set},
    Pervasives.format4 a Format.formatter unit (Lwt.t unit) -> a.

  Parameter lwt_warn : forall {a : Set},
    Pervasives.format4 a Format.formatter unit (Lwt.t unit) -> a.

  Parameter lwt_log_error : forall {a : Set},
    Pervasives.format4 a Format.formatter unit (Lwt.t unit) -> a.
End Logging.

Module Time.
  Parameter t : Set.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter add : t -> int64 -> t.

  Parameter diff : t -> t -> int64.

  Parameter of_seconds : int64 -> t.

  Parameter to_seconds : t -> int64.

  Parameter of_notation : string -> option t.

  Parameter of_notation_exn : string -> t.

  Parameter to_notation : t -> string.

  Parameter encoding : Data_encoding.t t.

  Parameter rfc_encoding : Data_encoding.t t.

  Parameter pp_hum : Format.formatter -> t -> unit.
End Time.

Module Option.
  Parameter map : forall {a b : Set}, (a -> b) -> option a -> option b.

  Parameter apply : forall {a b : Set}, (a -> option b) -> option a -> option b.

  Parameter iter : forall {a : Set}, (a -> unit) -> option a -> unit.

  Parameter unopt : forall {a : Set}, a -> option a -> a.

  Parameter unopt_map : forall {a b : Set}, (a -> b) -> b -> option a -> b.

  Parameter first_some : forall {a : Set}, option a -> option a -> option a.

  Parameter try_with : forall {a : Set}, (unit -> a) -> option a.

  Parameter some : forall {a : Set}, a -> option a.
End Option.

Module RPC_arg.
  Parameter t : forall (a : Set), Set.

  Definition arg (a : Set) := t a.

  Parameter make : forall {a : Set},
    option string -> string -> (string -> Pervasives.result a string) ->
    (a -> string) -> unit -> arg a.

  Module descr.
    Record record := {
      name : string;
      descr : option string }.
  End descr.
  Definition descr := descr.record.

  Parameter __descr_value : forall {a : Set}, arg a -> descr.

  Parameter int : arg Z.

  Parameter __int32_value : arg int32.

  Parameter __int64_value : arg int64.

  Parameter __float_value : arg Z.

  Parameter __string_value : arg string.

  Parameter like : forall {a : Set}, arg a -> option string -> string -> arg a.

  Reserved Notation "'eq".

  Inductive eq_gadt : Set :=
  | Eq : eq_gadt
  
  where "'eq" := (fun (a b : Set) => eq_gadt).

  Definition eq := 'eq.

  Parameter __eq_value : forall {a b : Set}, arg a -> arg b -> option (eq a b).
End RPC_arg.

Module RPC_path.
  Parameter t : forall (prefix params : Set), Set.

  Definition path (prefix params : Set) := t prefix params.

  Definition context (prefix : Set) := path prefix prefix.

  Parameter root : context unit.

  Parameter open_root : forall {a : Set}, context a.

  Parameter add_suffix : forall {params prefix : Set},
    path prefix params -> string -> path prefix params.

  Parameter op_div : forall {params prefix : Set},
    path prefix params -> string -> path prefix params.

  Parameter add_arg : forall {a params prefix : Set},
    path prefix params -> RPC_arg.t a -> path prefix (params * a).

  Parameter op_divcolon : forall {a params prefix : Set},
    path prefix params -> RPC_arg.t a -> path prefix (params * a).

  Parameter add_final_args : forall {a params prefix : Set},
    path prefix params -> RPC_arg.t a -> path prefix (params * list a).

  Parameter op_divcolonstar : forall {a params prefix : Set},
    path prefix params -> RPC_arg.t a -> path prefix (params * list a).
End RPC_path.

Module RPC_query.
  Parameter t : forall (a : Set), Set.

  Definition query (a : Set) := t a.

  Parameter empty : query unit.

  Parameter field : forall (a b : Set), Set.

  Parameter __field_value : forall {a b : Set},
    option string -> string -> RPC_arg.t a -> a -> (b -> a) -> field b a.

  Parameter opt_field : forall {a b : Set},
    option string -> string -> RPC_arg.t a -> (b -> option a) ->
    field b (option a).

  Parameter flag : forall {b : Set},
    option string -> string -> (b -> bool) -> field b bool.

  Parameter multi_field : forall {a b : Set},
    option string -> string -> RPC_arg.t a -> (b -> list a) -> field b (list a).

  Parameter open_query : forall (a b c : Set), Set.

  Parameter __query_value : forall {a b : Set}, b -> open_query a b b.

  Parameter op_pipeplus : forall {a b c d : Set},
    open_query a b (c -> d) -> field a c -> open_query a b d.

  Parameter seal : forall {a b : Set}, open_query a b a -> t a.

  Definition untyped := list (string * string).

  (* exception Invalid *)

  Parameter parse : forall {a : Set}, query a -> untyped -> a.
End RPC_query.

Module RPC_service.
  Inductive meth : Set :=
  | PUT : meth
  | GET : meth
  | DELETE : meth
  | POST : meth
  | PATCH : meth.

  Parameter t : forall
    (expected_variable prefix params query input output : Set), Set.

  Definition service (expected_variable prefix params query input output : Set)
    :=
    t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix params query input output.

  Parameter get_service : forall {output params prefix query : Set},
    option string -> RPC_query.t query -> Data_encoding.t output ->
    RPC_path.t prefix params ->
    service (* `GET *) unit prefix params query unit output.

  Parameter post_service : forall {input output params prefix query : Set},
    option string -> RPC_query.t query -> Data_encoding.t input ->
    Data_encoding.t output -> RPC_path.t prefix params ->
    service (* `POST *) unit prefix params query input output.

  Parameter delete_service : forall {output params prefix query : Set},
    option string -> RPC_query.t query -> Data_encoding.t output ->
    RPC_path.t prefix params ->
    service (* `DELETE *) unit prefix params query unit output.

  Parameter patch_service : forall {input output params prefix query : Set},
    option string -> RPC_query.t query -> Data_encoding.t input ->
    Data_encoding.t output -> RPC_path.t prefix params ->
    service (* `PATCH *) unit prefix params query input output.

  Parameter put_service : forall {input output params prefix query : Set},
    option string -> RPC_query.t query -> Data_encoding.t input ->
    Data_encoding.t output -> RPC_path.t prefix params ->
    service (* `PUT *) unit prefix params query input output.
End RPC_service.

Module RPC_answer.
  Reserved Notation "'stream".

  Module stream_skeleton.
    Record record {next shutdown : Set} := {
      next : next;
      shutdown : shutdown }.
    Arguments record : clear implicits.
  End stream_skeleton.
  Definition stream_skeleton := stream_skeleton.record.

  Inductive t (o : Set) : Set :=
  | OkStream : 'stream o -> t o
  | Unauthorized : option (list Error_monad.__error) -> t o
  | Error : option (list Error_monad.__error) -> t o
  | Ok : o -> t o
  | Not_found : option (list Error_monad.__error) -> t o
  | Forbidden : option (list Error_monad.__error) -> t o
  | Created : option string -> t o
  | Conflict : option (list Error_monad.__error) -> t o
  | No_content : t o
  
  where "'stream" := (fun (a : Set) =>
    stream_skeleton (unit -> Lwt.t (option a)) (unit -> unit)).

  Definition stream := 'stream.

  Arguments OkStream {_}.
  Arguments Unauthorized {_}.
  Arguments Error {_}.
  Arguments Ok {_}.
  Arguments Not_found {_}.
  Arguments Forbidden {_}.
  Arguments Created {_}.
  Arguments Conflict {_}.
  Arguments No_content {_}.

  Parameter __return : forall {o : Set}, o -> Lwt.t (t o).

  Parameter return_stream : forall {o : Set}, stream o -> Lwt.t (t o).

  Parameter not_found : forall {o : Set}, Lwt.t (t o).

  Parameter fail : forall {a : Set}, list Error_monad.__error -> Lwt.t (t a).
End RPC_answer.

Module RPC_directory.
  Parameter t : forall (prefix : Set), Set.

  Definition directory (prefix : Set) := t prefix.

  Parameter empty : forall {prefix : Set}, directory prefix.

  Parameter map : forall {a b : Set},
    (a -> Lwt.t b) -> directory b -> directory a.

  Parameter prefix : forall {p pr : Set},
    RPC_path.path pr p -> directory p -> directory pr.

  Parameter merge : forall {a : Set}, directory a -> directory a -> directory a.

  Inductive step : Set :=
  | Static : string -> step
  | Dynamic : RPC_arg.descr -> step
  | DynamicTail : RPC_arg.descr -> step.

  Inductive conflict : Set :=
  | CService : RPC_service.meth -> conflict
  | CDir : conflict
  | CBuilder : conflict
  | CTail : conflict
  | CTypes : RPC_arg.descr -> RPC_arg.descr -> conflict
  | CType : RPC_arg.descr -> list string -> conflict.

  (* exception Conflict *)

  Parameter register : forall {input output params prefix query : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix params query input output ->
    (params -> query -> input -> Lwt.t (Error_monad.tzresult output)) ->
    directory prefix.

  Parameter opt_register : forall {input output params prefix query : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix params query input output ->
    (params -> query -> input -> Lwt.t (Error_monad.tzresult (option output)))
    -> directory prefix.

  Parameter gen_register : forall {input output params prefix query : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix params query input output ->
    (params -> query -> input ->
    Lwt.t
      ((* `OkStream *) RPC_answer.stream output +
        (* `Unauthorized *) option (list Error_monad.__error) +
        (* `Error *) option (list Error_monad.__error) + (* `Ok *) output +
        (* `Not_found *) option (list Error_monad.__error) +
        (* `Forbidden *) option (list Error_monad.__error) +
        (* `Created *) option string +
        (* `Conflict *) option (list Error_monad.__error) +
        (* `No_content *) unit)) -> directory prefix.

  Parameter lwt_register : forall {input output params prefix query : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix params query input output ->
    (params -> query -> input -> Lwt.t output) -> directory prefix.

  Parameter register0 : forall {i o q : Set},
    directory unit ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) unit unit q i o ->
    (q -> i -> Lwt.t (Error_monad.tzresult o)) -> directory unit.

  Parameter register1 : forall {a i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (unit * a) q i o ->
    (a -> q -> i -> Lwt.t (Error_monad.tzresult o)) -> directory prefix.

  Parameter register2 : forall {a b i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix ((unit * a) * b) q i o ->
    (a -> b -> q -> i -> Lwt.t (Error_monad.tzresult o)) -> directory prefix.

  Parameter register3 : forall {a b c i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (((unit * a) * b) * c) q i o ->
    (a -> b -> c -> q -> i -> Lwt.t (Error_monad.tzresult o)) ->
    directory prefix.

  Parameter register4 : forall {a b c d i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix ((((unit * a) * b) * c) * d) q i o ->
    (a -> b -> c -> d -> q -> i -> Lwt.t (Error_monad.tzresult o)) ->
    directory prefix.

  Parameter register5 : forall {a b c d e i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (((((unit * a) * b) * c) * d) * e) q i o ->
    (a -> b -> c -> d -> e -> q -> i -> Lwt.t (Error_monad.tzresult o)) ->
    directory prefix.

  Parameter opt_register0 : forall {i o q : Set},
    directory unit ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) unit unit q i o ->
    (q -> i -> Lwt.t (Error_monad.tzresult (option o))) -> directory unit.

  Parameter opt_register1 : forall {a i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (unit * a) q i o ->
    (a -> q -> i -> Lwt.t (Error_monad.tzresult (option o))) -> directory prefix.

  Parameter opt_register2 : forall {a b i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix ((unit * a) * b) q i o ->
    (a -> b -> q -> i -> Lwt.t (Error_monad.tzresult (option o))) ->
    directory prefix.

  Parameter opt_register3 : forall {a b c i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (((unit * a) * b) * c) q i o ->
    (a -> b -> c -> q -> i -> Lwt.t (Error_monad.tzresult (option o))) ->
    directory prefix.

  Parameter opt_register4 : forall {a b c d i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix ((((unit * a) * b) * c) * d) q i o ->
    (a -> b -> c -> d -> q -> i -> Lwt.t (Error_monad.tzresult (option o))) ->
    directory prefix.

  Parameter opt_register5 : forall {a b c d e i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (((((unit * a) * b) * c) * d) * e) q i o ->
    (a -> b -> c -> d -> e -> q -> i -> Lwt.t (Error_monad.tzresult (option o)))
    -> directory prefix.

  Parameter gen_register0 : forall {i o q : Set},
    directory unit ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) unit unit q i o ->
    (q -> i ->
    Lwt.t
      ((* `OkStream *) RPC_answer.stream o +
        (* `Unauthorized *) option (list Error_monad.__error) +
        (* `Error *) option (list Error_monad.__error) + (* `Ok *) o +
        (* `Not_found *) option (list Error_monad.__error) +
        (* `Forbidden *) option (list Error_monad.__error) +
        (* `Created *) option string +
        (* `Conflict *) option (list Error_monad.__error) +
        (* `No_content *) unit)) -> directory unit.

  Parameter gen_register1 : forall {a i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (unit * a) q i o ->
    (a -> q -> i ->
    Lwt.t
      ((* `OkStream *) RPC_answer.stream o +
        (* `Unauthorized *) option (list Error_monad.__error) +
        (* `Error *) option (list Error_monad.__error) + (* `Ok *) o +
        (* `Not_found *) option (list Error_monad.__error) +
        (* `Forbidden *) option (list Error_monad.__error) +
        (* `Created *) option string +
        (* `Conflict *) option (list Error_monad.__error) +
        (* `No_content *) unit)) -> directory prefix.

  Parameter gen_register2 : forall {a b i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix ((unit * a) * b) q i o ->
    (a -> b -> q -> i ->
    Lwt.t
      ((* `OkStream *) RPC_answer.stream o +
        (* `Unauthorized *) option (list Error_monad.__error) +
        (* `Error *) option (list Error_monad.__error) + (* `Ok *) o +
        (* `Not_found *) option (list Error_monad.__error) +
        (* `Forbidden *) option (list Error_monad.__error) +
        (* `Created *) option string +
        (* `Conflict *) option (list Error_monad.__error) +
        (* `No_content *) unit)) -> directory prefix.

  Parameter gen_register3 : forall {a b c i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (((unit * a) * b) * c) q i o ->
    (a -> b -> c -> q -> i ->
    Lwt.t
      ((* `OkStream *) RPC_answer.stream o +
        (* `Unauthorized *) option (list Error_monad.__error) +
        (* `Error *) option (list Error_monad.__error) + (* `Ok *) o +
        (* `Not_found *) option (list Error_monad.__error) +
        (* `Forbidden *) option (list Error_monad.__error) +
        (* `Created *) option string +
        (* `Conflict *) option (list Error_monad.__error) +
        (* `No_content *) unit)) -> directory prefix.

  Parameter gen_register4 : forall {a b c d i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix ((((unit * a) * b) * c) * d) q i o ->
    (a -> b -> c -> d -> q -> i ->
    Lwt.t
      ((* `OkStream *) RPC_answer.stream o +
        (* `Unauthorized *) option (list Error_monad.__error) +
        (* `Error *) option (list Error_monad.__error) + (* `Ok *) o +
        (* `Not_found *) option (list Error_monad.__error) +
        (* `Forbidden *) option (list Error_monad.__error) +
        (* `Created *) option string +
        (* `Conflict *) option (list Error_monad.__error) +
        (* `No_content *) unit)) -> directory prefix.

  Parameter gen_register5 : forall {a b c d e i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (((((unit * a) * b) * c) * d) * e) q i o ->
    (a -> b -> c -> d -> e -> q -> i ->
    Lwt.t
      ((* `OkStream *) RPC_answer.stream o +
        (* `Unauthorized *) option (list Error_monad.__error) +
        (* `Error *) option (list Error_monad.__error) + (* `Ok *) o +
        (* `Not_found *) option (list Error_monad.__error) +
        (* `Forbidden *) option (list Error_monad.__error) +
        (* `Created *) option string +
        (* `Conflict *) option (list Error_monad.__error) +
        (* `No_content *) unit)) -> directory prefix.

  Parameter lwt_register0 : forall {i o q : Set},
    directory unit ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) unit unit q i o -> (q -> i -> Lwt.t o) ->
    directory unit.

  Parameter lwt_register1 : forall {a i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (unit * a) q i o ->
    (a -> q -> i -> Lwt.t o) -> directory prefix.

  Parameter lwt_register2 : forall {a b i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix ((unit * a) * b) q i o ->
    (a -> b -> q -> i -> Lwt.t o) -> directory prefix.

  Parameter lwt_register3 : forall {a b c i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (((unit * a) * b) * c) q i o ->
    (a -> b -> c -> q -> i -> Lwt.t o) -> directory prefix.

  Parameter lwt_register4 : forall {a b c d i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix ((((unit * a) * b) * c) * d) q i o ->
    (a -> b -> c -> d -> q -> i -> Lwt.t o) -> directory prefix.

  Parameter lwt_register5 : forall {a b c d e i o prefix q : Set},
    directory prefix ->
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) prefix (((((unit * a) * b) * c) * d) * e) q i o ->
    (a -> b -> c -> d -> e -> q -> i -> Lwt.t o) -> directory prefix.

  Parameter register_dynamic_directory : forall {a prefix : Set},
    option string -> directory prefix -> RPC_path.t prefix a ->
    (a -> Lwt.t (directory a)) -> directory prefix.
End RPC_directory.

Module Base58.
  Parameter encoding : forall (a : Set), Set.

  Parameter simple_decode : forall {a : Set}, encoding a -> string -> option a.

  Parameter simple_encode : forall {a : Set}, encoding a -> a -> string.

  Definition data := extensible_type.

  Parameter register_encoding : forall {a : Set},
    string -> Z -> (a -> string) -> (string -> option a) -> (a -> data) ->
    encoding a.

  Parameter check_encoded_prefix : forall {a : Set},
    encoding a -> string -> Z -> unit.

  Parameter decode : string -> option data.
End Base58.

Module S.
  Module T.
    Record signature {t : Set} := {
      t := t;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
      pp : Format.formatter -> t -> unit;
      encoding : Data_encoding.t t;
      to_bytes : t -> MBytes.t;
      of_bytes : MBytes.t -> option t;
    }.
    Arguments signature : clear implicits.
  End T.

  Module HASHABLE.
    Record signature {t hash : Set} := {
      t := t;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
      pp : Format.formatter -> t -> unit;
      encoding : Data_encoding.t t;
      to_bytes : t -> MBytes.t;
      of_bytes : MBytes.t -> option t;
      hash := hash;
      __hash_value : t -> hash;
      hash_raw : MBytes.t -> hash;
    }.
    Arguments signature : clear implicits.
  End HASHABLE.

  Module MINIMAL_HASH.
    Record signature {t : Set} := {
      t := t;
      name : string;
      title : string;
      pp : Format.formatter -> t -> unit;
      pp_short : Format.formatter -> t -> unit;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
      hash_bytes : option MBytes.t -> list MBytes.t -> t;
      hash_string : option string -> list string -> t;
      zero : t;
    }.
    Arguments signature : clear implicits.
  End MINIMAL_HASH.

  Module RAW_DATA.
    Record signature {t : Set} := {
      t := t;
      size : Z;
      to_bytes : t -> MBytes.t;
      of_bytes_opt : MBytes.t -> option t;
      of_bytes_exn : MBytes.t -> t;
    }.
    Arguments signature : clear implicits.
  End RAW_DATA.

  Module B58_DATA.
    Record signature {t : Set} := {
      t := t;
      to_b58check : t -> string;
      to_short_b58check : t -> string;
      of_b58check_exn : string -> t;
      of_b58check_opt : string -> option t;
      (* extensible_type Base58.data *)
      b58check_encoding : Base58.encoding t;
    }.
    Arguments signature : clear implicits.
  End B58_DATA.

  Module ENCODER.
    Record signature {t : Set} := {
      t := t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
    }.
    Arguments signature : clear implicits.
  End ENCODER.

  Module SET.
    Record signature {elt t : Set} := {
      elt := elt;
      t := t;
      empty : t;
      is_empty : t -> bool;
      mem : elt -> t -> bool;
      add : elt -> t -> t;
      singleton : elt -> t;
      remove : elt -> t -> t;
      union : t -> t -> t;
      inter : t -> t -> t;
      diff : t -> t -> t;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      subset : t -> t -> bool;
      iter : (elt -> unit) -> t -> unit;
      map : (elt -> elt) -> t -> t;
      fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a;
      for_all : (elt -> bool) -> t -> bool;
      __exists : (elt -> bool) -> t -> bool;
      filter : (elt -> bool) -> t -> t;
      partition : (elt -> bool) -> t -> t * t;
      cardinal : t -> Z;
      elements : t -> list elt;
      min_elt_opt : t -> option elt;
      max_elt_opt : t -> option elt;
      choose_opt : t -> option elt;
      split : elt -> t -> t * bool * t;
      find_opt : elt -> t -> option elt;
      find_first_opt : (elt -> bool) -> t -> option elt;
      find_last_opt : (elt -> bool) -> t -> option elt;
      of_list : list elt -> t;
    }.
    Arguments signature : clear implicits.
  End SET.

  Module MAP.
    Record signature {key : Set} {t : Set -> Set} := {
      key := key;
      t := t;
      empty : forall {a : Set}, t a;
      is_empty : forall {a : Set}, t a -> bool;
      mem : forall {a : Set}, key -> t a -> bool;
      add : forall {a : Set}, key -> a -> t a -> t a;
      update : forall {a : Set}, key -> (option a -> option a) -> t a -> t a;
      singleton : forall {a : Set}, key -> a -> t a;
      remove : forall {a : Set}, key -> t a -> t a;
      merge : forall {a b c : Set},
        (key -> option a -> option b -> option c) -> t a -> t b -> t c;
      union : forall {a : Set},
        (key -> a -> a -> option a) -> t a -> t a -> t a;
      compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z;
      equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool;
      iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit;
      fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b;
      for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool;
      __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool;
      filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a;
      partition : forall {a : Set}, (key -> a -> bool) -> t a -> t a * t a;
      cardinal : forall {a : Set}, t a -> Z;
      bindings : forall {a : Set}, t a -> list (key * a);
      min_binding_opt : forall {a : Set}, t a -> option (key * a);
      max_binding_opt : forall {a : Set}, t a -> option (key * a);
      choose_opt : forall {a : Set}, t a -> option (key * a);
      split : forall {a : Set}, key -> t a -> t a * option a * t a;
      find_opt : forall {a : Set}, key -> t a -> option a;
      find_first_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a);
      find_last_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a);
      map : forall {a b : Set}, (a -> b) -> t a -> t b;
      mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b;
    }.
    Arguments signature : clear implicits.
  End MAP.

  Module INDEXES_Set.
    Record signature {elt t : Set} := {
      elt := elt;
      t := t;
      empty : t;
      is_empty : t -> bool;
      mem : elt -> t -> bool;
      add : elt -> t -> t;
      singleton : elt -> t;
      remove : elt -> t -> t;
      union : t -> t -> t;
      inter : t -> t -> t;
      diff : t -> t -> t;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      subset : t -> t -> bool;
      iter : (elt -> unit) -> t -> unit;
      map : (elt -> elt) -> t -> t;
      fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a;
      for_all : (elt -> bool) -> t -> bool;
      __exists : (elt -> bool) -> t -> bool;
      filter : (elt -> bool) -> t -> t;
      partition : (elt -> bool) -> t -> t * t;
      cardinal : t -> Z;
      elements : t -> list elt;
      min_elt : t -> elt;
      min_elt_opt : t -> option elt;
      max_elt : t -> elt;
      max_elt_opt : t -> option elt;
      choose : t -> elt;
      choose_opt : t -> option elt;
      split : elt -> t -> t * bool * t;
      find : elt -> t -> elt;
      find_opt : elt -> t -> option elt;
      find_first : (elt -> bool) -> t -> elt;
      find_first_opt : (elt -> bool) -> t -> option elt;
      find_last : (elt -> bool) -> t -> elt;
      find_last_opt : (elt -> bool) -> t -> option elt;
      of_list : list elt -> t;
      to_seq_from : elt -> t -> OCaml.Seq.t elt;
      to_seq : t -> OCaml.Seq.t elt;
      add_seq : OCaml.Seq.t elt -> t -> t;
      of_seq : OCaml.Seq.t elt -> t;
      encoding : Data_encoding.t elt;
    }.
    Arguments signature : clear implicits.
  End INDEXES_Set.

  Module INDEXES_Map.
    Record signature {key : Set} {t : Set -> Set} := {
      key := key;
      t := t;
      empty : forall {a : Set}, t a;
      is_empty : forall {a : Set}, t a -> bool;
      mem : forall {a : Set}, key -> t a -> bool;
      add : forall {a : Set}, key -> a -> t a -> t a;
      update : forall {a : Set}, key -> (option a -> option a) -> t a -> t a;
      singleton : forall {a : Set}, key -> a -> t a;
      remove : forall {a : Set}, key -> t a -> t a;
      merge : forall {a b c : Set},
        (key -> option a -> option b -> option c) -> t a -> t b -> t c;
      union : forall {a : Set},
        (key -> a -> a -> option a) -> t a -> t a -> t a;
      compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z;
      equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool;
      iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit;
      fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b;
      for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool;
      __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool;
      filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a;
      partition : forall {a : Set}, (key -> a -> bool) -> t a -> t a * t a;
      cardinal : forall {a : Set}, t a -> Z;
      bindings : forall {a : Set}, t a -> list (key * a);
      min_binding : forall {a : Set}, t a -> key * a;
      min_binding_opt : forall {a : Set}, t a -> option (key * a);
      max_binding : forall {a : Set}, t a -> key * a;
      max_binding_opt : forall {a : Set}, t a -> option (key * a);
      choose : forall {a : Set}, t a -> key * a;
      choose_opt : forall {a : Set}, t a -> option (key * a);
      split : forall {a : Set}, key -> t a -> t a * option a * t a;
      find : forall {a : Set}, key -> t a -> a;
      find_opt : forall {a : Set}, key -> t a -> option a;
      find_first : forall {a : Set}, (key -> bool) -> t a -> key * a;
      find_first_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a);
      find_last : forall {a : Set}, (key -> bool) -> t a -> key * a;
      find_last_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a);
      map : forall {a b : Set}, (a -> b) -> t a -> t b;
      mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b;
      to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a);
      to_seq_from : forall {a : Set}, key -> t a -> OCaml.Seq.t (key * a);
      add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a;
      of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a;
      encoding : forall {a : Set}, Data_encoding.t a -> Data_encoding.t (t a);
    }.
    Arguments signature : clear implicits.
  End INDEXES_Map.

  Module INDEXES.
    Record signature {t __Set_t : Set} {Map_t : Set -> Set} := {
      t := t;
      to_path : t -> list string -> list string;
      of_path : list string -> option t;
      of_path_exn : list string -> t;
      prefix_path : string -> list string;
      path_length : Z;
      __Set : INDEXES_Set.signature t __Set_t;
      Map : INDEXES_Map.signature t Map_t;
    }.
    Arguments signature : clear implicits.
  End INDEXES.

  Module HASH.
    Record signature {t __Set_t : Set} {Map_t : Set -> Set} := {
      t := t;
      name : string;
      title : string;
      pp : Format.formatter -> t -> unit;
      pp_short : Format.formatter -> t -> unit;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
      hash_bytes : option MBytes.t -> list MBytes.t -> t;
      hash_string : option string -> list string -> t;
      zero : t;
      size : Z;
      to_bytes : t -> MBytes.t;
      of_bytes_opt : MBytes.t -> option t;
      of_bytes_exn : MBytes.t -> t;
      to_b58check : t -> string;
      to_short_b58check : t -> string;
      of_b58check_exn : string -> t;
      of_b58check_opt : string -> option t;
      (* extensible_type Base58.data *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      to_path : t -> list string -> list string;
      of_path : list string -> option t;
      of_path_exn : list string -> t;
      prefix_path : string -> list string;
      path_length : Z;
      (* module Set *)
      (* module Map *)
    }.
    Arguments signature : clear implicits.
  End HASH.

  Module MERKLE_TREE.
    Record signature {elt t __Set_t : Set} {Map_t : Set -> Set} {path : Set} :=
      {
      elt := elt;
      t := t;
      name : string;
      title : string;
      pp : Format.formatter -> t -> unit;
      pp_short : Format.formatter -> t -> unit;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
      hash_bytes : option MBytes.t -> list MBytes.t -> t;
      hash_string : option string -> list string -> t;
      zero : t;
      size : Z;
      to_bytes : t -> MBytes.t;
      of_bytes_opt : MBytes.t -> option t;
      of_bytes_exn : MBytes.t -> t;
      to_b58check : t -> string;
      to_short_b58check : t -> string;
      of_b58check_exn : string -> t;
      of_b58check_opt : string -> option t;
      (* extensible_type Base58.data *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      to_path : t -> list string -> list string;
      of_path : list string -> option t;
      of_path_exn : list string -> t;
      prefix_path : string -> list string;
      path_length : Z;
      (* module Set *)
      (* module Map *)
      compute : list elt -> t;
      empty : t;
      path := path;
      compute_path : list elt -> Z -> path;
      check_path : path -> elt -> t * Z;
      path_encoding : Data_encoding.t path;
    }.
    Arguments signature : clear implicits.
  End MERKLE_TREE.

  Module SIGNATURE_Public_key_hash.
    Record signature {t __Set_t : Set} {Map_t : Set -> Set} := {
      t := t;
      pp : Format.formatter -> t -> unit;
      pp_short : Format.formatter -> t -> unit;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
      size : Z;
      to_bytes : t -> MBytes.t;
      of_bytes_opt : MBytes.t -> option t;
      of_bytes_exn : MBytes.t -> t;
      to_b58check : t -> string;
      to_short_b58check : t -> string;
      of_b58check_exn : string -> t;
      of_b58check_opt : string -> option t;
      (* extensible_type Base58.data *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      to_path : t -> list string -> list string;
      of_path : list string -> option t;
      of_path_exn : list string -> t;
      prefix_path : string -> list string;
      path_length : Z;
      (* module Set *)
      (* module Map *)
      zero : t;
    }.
    Arguments signature : clear implicits.
  End SIGNATURE_Public_key_hash.

  Module SIGNATURE_Public_key.
    Record signature {t public_key_hash_t : Set} := {
      t := t;
      pp : Format.formatter -> t -> unit;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
      to_b58check : t -> string;
      to_short_b58check : t -> string;
      of_b58check_exn : string -> t;
      of_b58check_opt : string -> option t;
      (* extensible_type Base58.data *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      public_key_hash_t := public_key_hash_t;
      __hash_value : t -> public_key_hash_t;
    }.
    Arguments signature : clear implicits.
  End SIGNATURE_Public_key.

  Module SIGNATURE.
    Record signature {Public_key_hash_t Public_key_hash___Set_t : Set}
      {Public_key_hash_Map_t : Set -> Set} {Public_key_t t watermark : Set} := {
      Public_key_hash :
        SIGNATURE_Public_key_hash.signature Public_key_hash_t
          Public_key_hash___Set_t Public_key_hash_Map_t;
      Public_key :
        SIGNATURE_Public_key.signature Public_key_t
          Public_key_hash.(SIGNATURE_Public_key_hash.t);
      t := t;
      pp : Format.formatter -> t -> unit;
      size : Z;
      to_bytes : t -> MBytes.t;
      of_bytes_opt : MBytes.t -> option t;
      of_bytes_exn : MBytes.t -> t;
      op_eq : t -> t -> bool;
      op_ltgt : t -> t -> bool;
      op_lt : t -> t -> bool;
      op_lteq : t -> t -> bool;
      op_gteq : t -> t -> bool;
      op_gt : t -> t -> bool;
      compare : t -> t -> Z;
      equal : t -> t -> bool;
      max : t -> t -> t;
      min : t -> t -> t;
      to_b58check : t -> string;
      to_short_b58check : t -> string;
      of_b58check_exn : string -> t;
      of_b58check_opt : string -> option t;
      (* extensible_type Base58.data *)
      b58check_encoding : Base58.encoding t;
      encoding : Data_encoding.t t;
      rpc_arg : RPC_arg.t t;
      zero : t;
      watermark := watermark;
      check :
        option watermark -> Public_key.(SIGNATURE_Public_key.t) -> t ->
        MBytes.t -> bool;
    }.
    Arguments signature : clear implicits.
  End SIGNATURE.
End S.

Module __Set.
  Module OrderedType.
    Record signature {t : Set} := {
      t := t;
      compare : t -> t -> Z;
    }.
    Arguments signature : clear implicits.
  End OrderedType.

  Module Make.
    (* Unhandled functor *)
  End Make.
End __Set.

Module Map.
  Module OrderedType.
    Record signature {t : Set} := {
      t := t;
      compare : t -> t -> Z;
    }.
    Arguments signature : clear implicits.
  End OrderedType.

  Module Make.
    (* Unhandled functor *)
  End Make.
End Map.

Module Blake2B.
  Module Name.
    Record signature := {
      name : string;
      title : string;
      size : option Z;
    }.
  End Name.

  Module PrefixedName.
    Record signature := {
      name : string;
      title : string;
      size : option Z;
      b58check_prefix : string;
    }.
  End PrefixedName.

  Module Make_minimal.
    (* Unhandled functor *)
  End Make_minimal.

  Module Make.
    (* Unhandled functor *)
  End Make.
End Blake2B.

Module Ed25519.
  Module Public_key_hash.
    Parameter t : Set.

    Parameter pp : Format.formatter -> t -> unit.

    Parameter pp_short : Format.formatter -> t -> unit.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.

    Parameter size : Z.

    Parameter to_bytes : t -> MBytes.t.

    Parameter of_bytes_opt : MBytes.t -> option t.

    Parameter of_bytes_exn : MBytes.t -> t.

    Parameter to_b58check : t -> string.

    Parameter to_short_b58check : t -> string.

    Parameter of_b58check_exn : string -> t.

    Parameter of_b58check_opt : string -> option t.

    (* extensible_type Base58.data *)

    Parameter b58check_encoding : Base58.encoding t.

    Parameter encoding : Data_encoding.t t.

    Parameter rpc_arg : RPC_arg.t t.

    Parameter to_path : t -> list string -> list string.

    Parameter of_path : list string -> option t.

    Parameter of_path_exn : list string -> t.

    Parameter prefix_path : string -> list string.

    Parameter path_length : Z.

    Module __Set.
      Definition elt := t.

      Parameter t : Set.

      Parameter empty : t.

      Parameter is_empty : t -> bool.

      Parameter mem : elt -> t -> bool.

      Parameter add : elt -> t -> t.

      Parameter singleton : elt -> t.

      Parameter remove : elt -> t -> t.

      Parameter union : t -> t -> t.

      Parameter inter : t -> t -> t.

      Parameter diff : t -> t -> t.

      Parameter compare : t -> t -> Z.

      Parameter equal : t -> t -> bool.

      Parameter subset : t -> t -> bool.

      Parameter iter : (elt -> unit) -> t -> unit.

      Parameter map : (elt -> elt) -> t -> t.

      Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

      Parameter for_all : (elt -> bool) -> t -> bool.

      Parameter __exists : (elt -> bool) -> t -> bool.

      Parameter filter : (elt -> bool) -> t -> t.

      Parameter partition : (elt -> bool) -> t -> t * t.

      Parameter cardinal : t -> Z.

      Parameter elements : t -> list elt.

      Parameter min_elt : t -> elt.

      Parameter min_elt_opt : t -> option elt.

      Parameter max_elt : t -> elt.

      Parameter max_elt_opt : t -> option elt.

      Parameter choose : t -> elt.

      Parameter choose_opt : t -> option elt.

      Parameter split : elt -> t -> t * bool * t.

      Parameter find : elt -> t -> elt.

      Parameter find_opt : elt -> t -> option elt.

      Parameter find_first : (elt -> bool) -> t -> elt.

      Parameter find_first_opt : (elt -> bool) -> t -> option elt.

      Parameter find_last : (elt -> bool) -> t -> elt.

      Parameter find_last_opt : (elt -> bool) -> t -> option elt.

      Parameter of_list : list elt -> t.

      Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

      Parameter to_seq : t -> OCaml.Seq.t elt.

      Parameter add_seq : OCaml.Seq.t elt -> t -> t.

      Parameter of_seq : OCaml.Seq.t elt -> t.

      Parameter encoding : Data_encoding.t elt.
    End __Set.

    Module Map.
      Definition key := t.

      Parameter t : forall (a : Set), Set.

      Parameter empty : forall {a : Set}, t a.

      Parameter is_empty : forall {a : Set}, t a -> bool.

      Parameter mem : forall {a : Set}, key -> t a -> bool.

      Parameter add : forall {a : Set}, key -> a -> t a -> t a.

      Parameter update : forall {a : Set},
        key -> (option a -> option a) -> t a -> t a.

      Parameter singleton : forall {a : Set}, key -> a -> t a.

      Parameter remove : forall {a : Set}, key -> t a -> t a.

      Parameter merge : forall {a b c : Set},
        (key -> option a -> option b -> option c) -> t a -> t b -> t c.

      Parameter union : forall {a : Set},
        (key -> a -> a -> option a) -> t a -> t a -> t a.

      Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

      Parameter equal : forall {a : Set},
        (a -> a -> bool) -> t a -> t a -> bool.

      Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

      Parameter fold : forall {a b : Set},
        (key -> a -> b -> b) -> t a -> b -> b.

      Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

      Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

      Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

      Parameter partition : forall {a : Set},
        (key -> a -> bool) -> t a -> t a * t a.

      Parameter cardinal : forall {a : Set}, t a -> Z.

      Parameter bindings : forall {a : Set}, t a -> list (key * a).

      Parameter min_binding : forall {a : Set}, t a -> key * a.

      Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

      Parameter max_binding : forall {a : Set}, t a -> key * a.

      Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

      Parameter choose : forall {a : Set}, t a -> key * a.

      Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

      Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

      Parameter find : forall {a : Set}, key -> t a -> a.

      Parameter find_opt : forall {a : Set}, key -> t a -> option a.

      Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

      Parameter find_first_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a).

      Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

      Parameter find_last_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a).

      Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

      Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

      Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

      Parameter to_seq_from : forall {a : Set},
        key -> t a -> OCaml.Seq.t (key * a).

      Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

      Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

      Parameter encoding : forall {a : Set},
        Data_encoding.t a -> Data_encoding.t (t a).
    End Map.

    Parameter zero : t.
  End Public_key_hash.

  Module Public_key.
    Parameter t : Set.

    Parameter pp : Format.formatter -> t -> unit.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.

    Parameter to_b58check : t -> string.

    Parameter to_short_b58check : t -> string.

    Parameter of_b58check_exn : string -> t.

    Parameter of_b58check_opt : string -> option t.

    (* extensible_type Base58.data *)

    Parameter b58check_encoding : Base58.encoding t.

    Parameter encoding : Data_encoding.t t.

    Parameter rpc_arg : RPC_arg.t t.

    Definition public_key_hash_t := Public_key_hash.t.

    Parameter __hash_value : t -> public_key_hash_t.
  End Public_key.

  Parameter t : Set.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter zero : t.

  Parameter check : option MBytes.t -> Public_key.t -> t -> MBytes.t -> bool.
End Ed25519.

Module Secp256k1.
  Module Public_key_hash.
    Parameter t : Set.

    Parameter pp : Format.formatter -> t -> unit.

    Parameter pp_short : Format.formatter -> t -> unit.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.

    Parameter size : Z.

    Parameter to_bytes : t -> MBytes.t.

    Parameter of_bytes_opt : MBytes.t -> option t.

    Parameter of_bytes_exn : MBytes.t -> t.

    Parameter to_b58check : t -> string.

    Parameter to_short_b58check : t -> string.

    Parameter of_b58check_exn : string -> t.

    Parameter of_b58check_opt : string -> option t.

    (* extensible_type Base58.data *)

    Parameter b58check_encoding : Base58.encoding t.

    Parameter encoding : Data_encoding.t t.

    Parameter rpc_arg : RPC_arg.t t.

    Parameter to_path : t -> list string -> list string.

    Parameter of_path : list string -> option t.

    Parameter of_path_exn : list string -> t.

    Parameter prefix_path : string -> list string.

    Parameter path_length : Z.

    Module __Set.
      Definition elt := t.

      Parameter t : Set.

      Parameter empty : t.

      Parameter is_empty : t -> bool.

      Parameter mem : elt -> t -> bool.

      Parameter add : elt -> t -> t.

      Parameter singleton : elt -> t.

      Parameter remove : elt -> t -> t.

      Parameter union : t -> t -> t.

      Parameter inter : t -> t -> t.

      Parameter diff : t -> t -> t.

      Parameter compare : t -> t -> Z.

      Parameter equal : t -> t -> bool.

      Parameter subset : t -> t -> bool.

      Parameter iter : (elt -> unit) -> t -> unit.

      Parameter map : (elt -> elt) -> t -> t.

      Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

      Parameter for_all : (elt -> bool) -> t -> bool.

      Parameter __exists : (elt -> bool) -> t -> bool.

      Parameter filter : (elt -> bool) -> t -> t.

      Parameter partition : (elt -> bool) -> t -> t * t.

      Parameter cardinal : t -> Z.

      Parameter elements : t -> list elt.

      Parameter min_elt : t -> elt.

      Parameter min_elt_opt : t -> option elt.

      Parameter max_elt : t -> elt.

      Parameter max_elt_opt : t -> option elt.

      Parameter choose : t -> elt.

      Parameter choose_opt : t -> option elt.

      Parameter split : elt -> t -> t * bool * t.

      Parameter find : elt -> t -> elt.

      Parameter find_opt : elt -> t -> option elt.

      Parameter find_first : (elt -> bool) -> t -> elt.

      Parameter find_first_opt : (elt -> bool) -> t -> option elt.

      Parameter find_last : (elt -> bool) -> t -> elt.

      Parameter find_last_opt : (elt -> bool) -> t -> option elt.

      Parameter of_list : list elt -> t.

      Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

      Parameter to_seq : t -> OCaml.Seq.t elt.

      Parameter add_seq : OCaml.Seq.t elt -> t -> t.

      Parameter of_seq : OCaml.Seq.t elt -> t.

      Parameter encoding : Data_encoding.t elt.
    End __Set.

    Module Map.
      Definition key := t.

      Parameter t : forall (a : Set), Set.

      Parameter empty : forall {a : Set}, t a.

      Parameter is_empty : forall {a : Set}, t a -> bool.

      Parameter mem : forall {a : Set}, key -> t a -> bool.

      Parameter add : forall {a : Set}, key -> a -> t a -> t a.

      Parameter update : forall {a : Set},
        key -> (option a -> option a) -> t a -> t a.

      Parameter singleton : forall {a : Set}, key -> a -> t a.

      Parameter remove : forall {a : Set}, key -> t a -> t a.

      Parameter merge : forall {a b c : Set},
        (key -> option a -> option b -> option c) -> t a -> t b -> t c.

      Parameter union : forall {a : Set},
        (key -> a -> a -> option a) -> t a -> t a -> t a.

      Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

      Parameter equal : forall {a : Set},
        (a -> a -> bool) -> t a -> t a -> bool.

      Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

      Parameter fold : forall {a b : Set},
        (key -> a -> b -> b) -> t a -> b -> b.

      Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

      Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

      Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

      Parameter partition : forall {a : Set},
        (key -> a -> bool) -> t a -> t a * t a.

      Parameter cardinal : forall {a : Set}, t a -> Z.

      Parameter bindings : forall {a : Set}, t a -> list (key * a).

      Parameter min_binding : forall {a : Set}, t a -> key * a.

      Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

      Parameter max_binding : forall {a : Set}, t a -> key * a.

      Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

      Parameter choose : forall {a : Set}, t a -> key * a.

      Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

      Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

      Parameter find : forall {a : Set}, key -> t a -> a.

      Parameter find_opt : forall {a : Set}, key -> t a -> option a.

      Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

      Parameter find_first_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a).

      Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

      Parameter find_last_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a).

      Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

      Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

      Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

      Parameter to_seq_from : forall {a : Set},
        key -> t a -> OCaml.Seq.t (key * a).

      Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

      Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

      Parameter encoding : forall {a : Set},
        Data_encoding.t a -> Data_encoding.t (t a).
    End Map.

    Parameter zero : t.
  End Public_key_hash.

  Module Public_key.
    Parameter t : Set.

    Parameter pp : Format.formatter -> t -> unit.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.

    Parameter to_b58check : t -> string.

    Parameter to_short_b58check : t -> string.

    Parameter of_b58check_exn : string -> t.

    Parameter of_b58check_opt : string -> option t.

    (* extensible_type Base58.data *)

    Parameter b58check_encoding : Base58.encoding t.

    Parameter encoding : Data_encoding.t t.

    Parameter rpc_arg : RPC_arg.t t.

    Definition public_key_hash_t := Public_key_hash.t.

    Parameter __hash_value : t -> public_key_hash_t.
  End Public_key.

  Parameter t : Set.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter zero : t.

  Parameter check : option MBytes.t -> Public_key.t -> t -> MBytes.t -> bool.
End Secp256k1.

Module P256.
  Module Public_key_hash.
    Parameter t : Set.

    Parameter pp : Format.formatter -> t -> unit.

    Parameter pp_short : Format.formatter -> t -> unit.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.

    Parameter size : Z.

    Parameter to_bytes : t -> MBytes.t.

    Parameter of_bytes_opt : MBytes.t -> option t.

    Parameter of_bytes_exn : MBytes.t -> t.

    Parameter to_b58check : t -> string.

    Parameter to_short_b58check : t -> string.

    Parameter of_b58check_exn : string -> t.

    Parameter of_b58check_opt : string -> option t.

    (* extensible_type Base58.data *)

    Parameter b58check_encoding : Base58.encoding t.

    Parameter encoding : Data_encoding.t t.

    Parameter rpc_arg : RPC_arg.t t.

    Parameter to_path : t -> list string -> list string.

    Parameter of_path : list string -> option t.

    Parameter of_path_exn : list string -> t.

    Parameter prefix_path : string -> list string.

    Parameter path_length : Z.

    Module __Set.
      Definition elt := t.

      Parameter t : Set.

      Parameter empty : t.

      Parameter is_empty : t -> bool.

      Parameter mem : elt -> t -> bool.

      Parameter add : elt -> t -> t.

      Parameter singleton : elt -> t.

      Parameter remove : elt -> t -> t.

      Parameter union : t -> t -> t.

      Parameter inter : t -> t -> t.

      Parameter diff : t -> t -> t.

      Parameter compare : t -> t -> Z.

      Parameter equal : t -> t -> bool.

      Parameter subset : t -> t -> bool.

      Parameter iter : (elt -> unit) -> t -> unit.

      Parameter map : (elt -> elt) -> t -> t.

      Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

      Parameter for_all : (elt -> bool) -> t -> bool.

      Parameter __exists : (elt -> bool) -> t -> bool.

      Parameter filter : (elt -> bool) -> t -> t.

      Parameter partition : (elt -> bool) -> t -> t * t.

      Parameter cardinal : t -> Z.

      Parameter elements : t -> list elt.

      Parameter min_elt : t -> elt.

      Parameter min_elt_opt : t -> option elt.

      Parameter max_elt : t -> elt.

      Parameter max_elt_opt : t -> option elt.

      Parameter choose : t -> elt.

      Parameter choose_opt : t -> option elt.

      Parameter split : elt -> t -> t * bool * t.

      Parameter find : elt -> t -> elt.

      Parameter find_opt : elt -> t -> option elt.

      Parameter find_first : (elt -> bool) -> t -> elt.

      Parameter find_first_opt : (elt -> bool) -> t -> option elt.

      Parameter find_last : (elt -> bool) -> t -> elt.

      Parameter find_last_opt : (elt -> bool) -> t -> option elt.

      Parameter of_list : list elt -> t.

      Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

      Parameter to_seq : t -> OCaml.Seq.t elt.

      Parameter add_seq : OCaml.Seq.t elt -> t -> t.

      Parameter of_seq : OCaml.Seq.t elt -> t.

      Parameter encoding : Data_encoding.t elt.
    End __Set.

    Module Map.
      Definition key := t.

      Parameter t : forall (a : Set), Set.

      Parameter empty : forall {a : Set}, t a.

      Parameter is_empty : forall {a : Set}, t a -> bool.

      Parameter mem : forall {a : Set}, key -> t a -> bool.

      Parameter add : forall {a : Set}, key -> a -> t a -> t a.

      Parameter update : forall {a : Set},
        key -> (option a -> option a) -> t a -> t a.

      Parameter singleton : forall {a : Set}, key -> a -> t a.

      Parameter remove : forall {a : Set}, key -> t a -> t a.

      Parameter merge : forall {a b c : Set},
        (key -> option a -> option b -> option c) -> t a -> t b -> t c.

      Parameter union : forall {a : Set},
        (key -> a -> a -> option a) -> t a -> t a -> t a.

      Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

      Parameter equal : forall {a : Set},
        (a -> a -> bool) -> t a -> t a -> bool.

      Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

      Parameter fold : forall {a b : Set},
        (key -> a -> b -> b) -> t a -> b -> b.

      Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

      Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

      Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

      Parameter partition : forall {a : Set},
        (key -> a -> bool) -> t a -> t a * t a.

      Parameter cardinal : forall {a : Set}, t a -> Z.

      Parameter bindings : forall {a : Set}, t a -> list (key * a).

      Parameter min_binding : forall {a : Set}, t a -> key * a.

      Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

      Parameter max_binding : forall {a : Set}, t a -> key * a.

      Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

      Parameter choose : forall {a : Set}, t a -> key * a.

      Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

      Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

      Parameter find : forall {a : Set}, key -> t a -> a.

      Parameter find_opt : forall {a : Set}, key -> t a -> option a.

      Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

      Parameter find_first_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a).

      Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

      Parameter find_last_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a).

      Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

      Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

      Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

      Parameter to_seq_from : forall {a : Set},
        key -> t a -> OCaml.Seq.t (key * a).

      Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

      Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

      Parameter encoding : forall {a : Set},
        Data_encoding.t a -> Data_encoding.t (t a).
    End Map.

    Parameter zero : t.
  End Public_key_hash.

  Module Public_key.
    Parameter t : Set.

    Parameter pp : Format.formatter -> t -> unit.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.

    Parameter to_b58check : t -> string.

    Parameter to_short_b58check : t -> string.

    Parameter of_b58check_exn : string -> t.

    Parameter of_b58check_opt : string -> option t.

    (* extensible_type Base58.data *)

    Parameter b58check_encoding : Base58.encoding t.

    Parameter encoding : Data_encoding.t t.

    Parameter rpc_arg : RPC_arg.t t.

    Definition public_key_hash_t := Public_key_hash.t.

    Parameter __hash_value : t -> public_key_hash_t.
  End Public_key.

  Parameter t : Set.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter zero : t.

  Parameter check : option MBytes.t -> Public_key.t -> t -> MBytes.t -> bool.
End P256.

Module Chain_id.
  Parameter t : Set.

  Parameter name : string.

  Parameter title : string.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter pp_short : Format.formatter -> t -> unit.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter hash_bytes : option MBytes.t -> list MBytes.t -> t.

  Parameter hash_string : option string -> list string -> t.

  Parameter zero : t.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter to_path : t -> list string -> list string.

  Parameter of_path : list string -> option t.

  Parameter of_path_exn : list string -> t.

  Parameter prefix_path : string -> list string.

  Parameter path_length : Z.

  Module __Set.
    Definition elt := t.

    Parameter t : Set.

    Parameter empty : t.

    Parameter is_empty : t -> bool.

    Parameter mem : elt -> t -> bool.

    Parameter add : elt -> t -> t.

    Parameter singleton : elt -> t.

    Parameter remove : elt -> t -> t.

    Parameter union : t -> t -> t.

    Parameter inter : t -> t -> t.

    Parameter diff : t -> t -> t.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter subset : t -> t -> bool.

    Parameter iter : (elt -> unit) -> t -> unit.

    Parameter map : (elt -> elt) -> t -> t.

    Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

    Parameter for_all : (elt -> bool) -> t -> bool.

    Parameter __exists : (elt -> bool) -> t -> bool.

    Parameter filter : (elt -> bool) -> t -> t.

    Parameter partition : (elt -> bool) -> t -> t * t.

    Parameter cardinal : t -> Z.

    Parameter elements : t -> list elt.

    Parameter min_elt : t -> elt.

    Parameter min_elt_opt : t -> option elt.

    Parameter max_elt : t -> elt.

    Parameter max_elt_opt : t -> option elt.

    Parameter choose : t -> elt.

    Parameter choose_opt : t -> option elt.

    Parameter split : elt -> t -> t * bool * t.

    Parameter find : elt -> t -> elt.

    Parameter find_opt : elt -> t -> option elt.

    Parameter find_first : (elt -> bool) -> t -> elt.

    Parameter find_first_opt : (elt -> bool) -> t -> option elt.

    Parameter find_last : (elt -> bool) -> t -> elt.

    Parameter find_last_opt : (elt -> bool) -> t -> option elt.

    Parameter of_list : list elt -> t.

    Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

    Parameter to_seq : t -> OCaml.Seq.t elt.

    Parameter add_seq : OCaml.Seq.t elt -> t -> t.

    Parameter of_seq : OCaml.Seq.t elt -> t.

    Parameter encoding : Data_encoding.t elt.
  End __Set.

  Module Map.
    Definition key := t.

    Parameter t : forall (a : Set), Set.

    Parameter empty : forall {a : Set}, t a.

    Parameter is_empty : forall {a : Set}, t a -> bool.

    Parameter mem : forall {a : Set}, key -> t a -> bool.

    Parameter add : forall {a : Set}, key -> a -> t a -> t a.

    Parameter update : forall {a : Set},
      key -> (option a -> option a) -> t a -> t a.

    Parameter singleton : forall {a : Set}, key -> a -> t a.

    Parameter remove : forall {a : Set}, key -> t a -> t a.

    Parameter merge : forall {a b c : Set},
      (key -> option a -> option b -> option c) -> t a -> t b -> t c.

    Parameter union : forall {a : Set},
      (key -> a -> a -> option a) -> t a -> t a -> t a.

    Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

    Parameter equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool.

    Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

    Parameter fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b.

    Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

    Parameter partition : forall {a : Set},
      (key -> a -> bool) -> t a -> t a * t a.

    Parameter cardinal : forall {a : Set}, t a -> Z.

    Parameter bindings : forall {a : Set}, t a -> list (key * a).

    Parameter min_binding : forall {a : Set}, t a -> key * a.

    Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter max_binding : forall {a : Set}, t a -> key * a.

    Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter choose : forall {a : Set}, t a -> key * a.

    Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

    Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

    Parameter find : forall {a : Set}, key -> t a -> a.

    Parameter find_opt : forall {a : Set}, key -> t a -> option a.

    Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_first_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_last_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

    Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

    Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

    Parameter to_seq_from : forall {a : Set},
      key -> t a -> OCaml.Seq.t (key * a).

    Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

    Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

    Parameter encoding : forall {a : Set},
      Data_encoding.t a -> Data_encoding.t (t a).
  End Map.
End Chain_id.

Module Signature.
  Inductive public_key_hash : Set :=
  | Ed25519Hash : Ed25519.Public_key_hash.t -> public_key_hash
  | Secp256k1Hash : Secp256k1.Public_key_hash.t -> public_key_hash
  | P256Hash : P256.Public_key_hash.t -> public_key_hash.

  Inductive public_key : Set :=
  | Ed25519 : Ed25519.Public_key.t -> public_key
  | Secp256k1 : Secp256k1.Public_key.t -> public_key
  | P256 : P256.Public_key.t -> public_key.

  Inductive watermark : Set :=
  | Block_header : Chain_id.t -> watermark
  | Endorsement : Chain_id.t -> watermark
  | Generic_operation : watermark
  | Custom : MBytes.t -> watermark.

  Module Public_key_hash.
    Definition t := public_key_hash.

    Parameter pp : Format.formatter -> t -> unit.

    Parameter pp_short : Format.formatter -> t -> unit.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.

    Parameter size : Z.

    Parameter to_bytes : t -> MBytes.t.

    Parameter of_bytes_opt : MBytes.t -> option t.

    Parameter of_bytes_exn : MBytes.t -> t.

    Parameter to_b58check : t -> string.

    Parameter to_short_b58check : t -> string.

    Parameter of_b58check_exn : string -> t.

    Parameter of_b58check_opt : string -> option t.

    (* extensible_type Base58.data *)

    Parameter b58check_encoding : Base58.encoding t.

    Parameter encoding : Data_encoding.t t.

    Parameter rpc_arg : RPC_arg.t t.

    Parameter to_path : t -> list string -> list string.

    Parameter of_path : list string -> option t.

    Parameter of_path_exn : list string -> t.

    Parameter prefix_path : string -> list string.

    Parameter path_length : Z.

    Module __Set.
      Definition elt := t.

      Parameter t : Set.

      Parameter empty : t.

      Parameter is_empty : t -> bool.

      Parameter mem : elt -> t -> bool.

      Parameter add : elt -> t -> t.

      Parameter singleton : elt -> t.

      Parameter remove : elt -> t -> t.

      Parameter union : t -> t -> t.

      Parameter inter : t -> t -> t.

      Parameter diff : t -> t -> t.

      Parameter compare : t -> t -> Z.

      Parameter equal : t -> t -> bool.

      Parameter subset : t -> t -> bool.

      Parameter iter : (elt -> unit) -> t -> unit.

      Parameter map : (elt -> elt) -> t -> t.

      Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

      Parameter for_all : (elt -> bool) -> t -> bool.

      Parameter __exists : (elt -> bool) -> t -> bool.

      Parameter filter : (elt -> bool) -> t -> t.

      Parameter partition : (elt -> bool) -> t -> t * t.

      Parameter cardinal : t -> Z.

      Parameter elements : t -> list elt.

      Parameter min_elt : t -> elt.

      Parameter min_elt_opt : t -> option elt.

      Parameter max_elt : t -> elt.

      Parameter max_elt_opt : t -> option elt.

      Parameter choose : t -> elt.

      Parameter choose_opt : t -> option elt.

      Parameter split : elt -> t -> t * bool * t.

      Parameter find : elt -> t -> elt.

      Parameter find_opt : elt -> t -> option elt.

      Parameter find_first : (elt -> bool) -> t -> elt.

      Parameter find_first_opt : (elt -> bool) -> t -> option elt.

      Parameter find_last : (elt -> bool) -> t -> elt.

      Parameter find_last_opt : (elt -> bool) -> t -> option elt.

      Parameter of_list : list elt -> t.

      Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

      Parameter to_seq : t -> OCaml.Seq.t elt.

      Parameter add_seq : OCaml.Seq.t elt -> t -> t.

      Parameter of_seq : OCaml.Seq.t elt -> t.

      Parameter encoding : Data_encoding.t elt.
    End __Set.

    Module Map.
      Definition key := t.

      Parameter t : forall (a : Set), Set.

      Parameter empty : forall {a : Set}, t a.

      Parameter is_empty : forall {a : Set}, t a -> bool.

      Parameter mem : forall {a : Set}, key -> t a -> bool.

      Parameter add : forall {a : Set}, key -> a -> t a -> t a.

      Parameter update : forall {a : Set},
        key -> (option a -> option a) -> t a -> t a.

      Parameter singleton : forall {a : Set}, key -> a -> t a.

      Parameter remove : forall {a : Set}, key -> t a -> t a.

      Parameter merge : forall {a b c : Set},
        (key -> option a -> option b -> option c) -> t a -> t b -> t c.

      Parameter union : forall {a : Set},
        (key -> a -> a -> option a) -> t a -> t a -> t a.

      Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

      Parameter equal : forall {a : Set},
        (a -> a -> bool) -> t a -> t a -> bool.

      Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

      Parameter fold : forall {a b : Set},
        (key -> a -> b -> b) -> t a -> b -> b.

      Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

      Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

      Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

      Parameter partition : forall {a : Set},
        (key -> a -> bool) -> t a -> t a * t a.

      Parameter cardinal : forall {a : Set}, t a -> Z.

      Parameter bindings : forall {a : Set}, t a -> list (key * a).

      Parameter min_binding : forall {a : Set}, t a -> key * a.

      Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

      Parameter max_binding : forall {a : Set}, t a -> key * a.

      Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

      Parameter choose : forall {a : Set}, t a -> key * a.

      Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

      Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

      Parameter find : forall {a : Set}, key -> t a -> a.

      Parameter find_opt : forall {a : Set}, key -> t a -> option a.

      Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

      Parameter find_first_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a).

      Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

      Parameter find_last_opt : forall {a : Set},
        (key -> bool) -> t a -> option (key * a).

      Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

      Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

      Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

      Parameter to_seq_from : forall {a : Set},
        key -> t a -> OCaml.Seq.t (key * a).

      Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

      Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

      Parameter encoding : forall {a : Set},
        Data_encoding.t a -> Data_encoding.t (t a).
    End Map.

    Parameter zero : t.
  End Public_key_hash.

  Module Public_key.
    Definition t := public_key.

    Parameter pp : Format.formatter -> t -> unit.

    Parameter op_eq : t -> t -> bool.

    Parameter op_ltgt : t -> t -> bool.

    Parameter op_lt : t -> t -> bool.

    Parameter op_lteq : t -> t -> bool.

    Parameter op_gteq : t -> t -> bool.

    Parameter op_gt : t -> t -> bool.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter max : t -> t -> t.

    Parameter min : t -> t -> t.

    Parameter to_b58check : t -> string.

    Parameter to_short_b58check : t -> string.

    Parameter of_b58check_exn : string -> t.

    Parameter of_b58check_opt : string -> option t.

    (* extensible_type Base58.data *)

    Parameter b58check_encoding : Base58.encoding t.

    Parameter encoding : Data_encoding.t t.

    Parameter rpc_arg : RPC_arg.t t.

    Definition public_key_hash_t := Public_key_hash.t.

    Parameter __hash_value : t -> public_key_hash_t.
  End Public_key.

  Parameter t : Set.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter zero : t.

  Parameter check : option watermark -> Public_key.t -> t -> MBytes.t -> bool.
End Signature.

Module Block_hash.
  Parameter t : Set.

  Parameter name : string.

  Parameter title : string.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter pp_short : Format.formatter -> t -> unit.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter hash_bytes : option MBytes.t -> list MBytes.t -> t.

  Parameter hash_string : option string -> list string -> t.

  Parameter zero : t.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter to_path : t -> list string -> list string.

  Parameter of_path : list string -> option t.

  Parameter of_path_exn : list string -> t.

  Parameter prefix_path : string -> list string.

  Parameter path_length : Z.

  Module __Set.
    Definition elt := t.

    Parameter t : Set.

    Parameter empty : t.

    Parameter is_empty : t -> bool.

    Parameter mem : elt -> t -> bool.

    Parameter add : elt -> t -> t.

    Parameter singleton : elt -> t.

    Parameter remove : elt -> t -> t.

    Parameter union : t -> t -> t.

    Parameter inter : t -> t -> t.

    Parameter diff : t -> t -> t.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter subset : t -> t -> bool.

    Parameter iter : (elt -> unit) -> t -> unit.

    Parameter map : (elt -> elt) -> t -> t.

    Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

    Parameter for_all : (elt -> bool) -> t -> bool.

    Parameter __exists : (elt -> bool) -> t -> bool.

    Parameter filter : (elt -> bool) -> t -> t.

    Parameter partition : (elt -> bool) -> t -> t * t.

    Parameter cardinal : t -> Z.

    Parameter elements : t -> list elt.

    Parameter min_elt : t -> elt.

    Parameter min_elt_opt : t -> option elt.

    Parameter max_elt : t -> elt.

    Parameter max_elt_opt : t -> option elt.

    Parameter choose : t -> elt.

    Parameter choose_opt : t -> option elt.

    Parameter split : elt -> t -> t * bool * t.

    Parameter find : elt -> t -> elt.

    Parameter find_opt : elt -> t -> option elt.

    Parameter find_first : (elt -> bool) -> t -> elt.

    Parameter find_first_opt : (elt -> bool) -> t -> option elt.

    Parameter find_last : (elt -> bool) -> t -> elt.

    Parameter find_last_opt : (elt -> bool) -> t -> option elt.

    Parameter of_list : list elt -> t.

    Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

    Parameter to_seq : t -> OCaml.Seq.t elt.

    Parameter add_seq : OCaml.Seq.t elt -> t -> t.

    Parameter of_seq : OCaml.Seq.t elt -> t.

    Parameter encoding : Data_encoding.t elt.
  End __Set.

  Module Map.
    Definition key := t.

    Parameter t : forall (a : Set), Set.

    Parameter empty : forall {a : Set}, t a.

    Parameter is_empty : forall {a : Set}, t a -> bool.

    Parameter mem : forall {a : Set}, key -> t a -> bool.

    Parameter add : forall {a : Set}, key -> a -> t a -> t a.

    Parameter update : forall {a : Set},
      key -> (option a -> option a) -> t a -> t a.

    Parameter singleton : forall {a : Set}, key -> a -> t a.

    Parameter remove : forall {a : Set}, key -> t a -> t a.

    Parameter merge : forall {a b c : Set},
      (key -> option a -> option b -> option c) -> t a -> t b -> t c.

    Parameter union : forall {a : Set},
      (key -> a -> a -> option a) -> t a -> t a -> t a.

    Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

    Parameter equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool.

    Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

    Parameter fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b.

    Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

    Parameter partition : forall {a : Set},
      (key -> a -> bool) -> t a -> t a * t a.

    Parameter cardinal : forall {a : Set}, t a -> Z.

    Parameter bindings : forall {a : Set}, t a -> list (key * a).

    Parameter min_binding : forall {a : Set}, t a -> key * a.

    Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter max_binding : forall {a : Set}, t a -> key * a.

    Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter choose : forall {a : Set}, t a -> key * a.

    Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

    Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

    Parameter find : forall {a : Set}, key -> t a -> a.

    Parameter find_opt : forall {a : Set}, key -> t a -> option a.

    Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_first_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_last_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

    Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

    Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

    Parameter to_seq_from : forall {a : Set},
      key -> t a -> OCaml.Seq.t (key * a).

    Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

    Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

    Parameter encoding : forall {a : Set},
      Data_encoding.t a -> Data_encoding.t (t a).
  End Map.
End Block_hash.

Module Operation_hash.
  Parameter t : Set.

  Parameter name : string.

  Parameter title : string.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter pp_short : Format.formatter -> t -> unit.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter hash_bytes : option MBytes.t -> list MBytes.t -> t.

  Parameter hash_string : option string -> list string -> t.

  Parameter zero : t.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter to_path : t -> list string -> list string.

  Parameter of_path : list string -> option t.

  Parameter of_path_exn : list string -> t.

  Parameter prefix_path : string -> list string.

  Parameter path_length : Z.

  Module __Set.
    Definition elt := t.

    Parameter t : Set.

    Parameter empty : t.

    Parameter is_empty : t -> bool.

    Parameter mem : elt -> t -> bool.

    Parameter add : elt -> t -> t.

    Parameter singleton : elt -> t.

    Parameter remove : elt -> t -> t.

    Parameter union : t -> t -> t.

    Parameter inter : t -> t -> t.

    Parameter diff : t -> t -> t.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter subset : t -> t -> bool.

    Parameter iter : (elt -> unit) -> t -> unit.

    Parameter map : (elt -> elt) -> t -> t.

    Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

    Parameter for_all : (elt -> bool) -> t -> bool.

    Parameter __exists : (elt -> bool) -> t -> bool.

    Parameter filter : (elt -> bool) -> t -> t.

    Parameter partition : (elt -> bool) -> t -> t * t.

    Parameter cardinal : t -> Z.

    Parameter elements : t -> list elt.

    Parameter min_elt : t -> elt.

    Parameter min_elt_opt : t -> option elt.

    Parameter max_elt : t -> elt.

    Parameter max_elt_opt : t -> option elt.

    Parameter choose : t -> elt.

    Parameter choose_opt : t -> option elt.

    Parameter split : elt -> t -> t * bool * t.

    Parameter find : elt -> t -> elt.

    Parameter find_opt : elt -> t -> option elt.

    Parameter find_first : (elt -> bool) -> t -> elt.

    Parameter find_first_opt : (elt -> bool) -> t -> option elt.

    Parameter find_last : (elt -> bool) -> t -> elt.

    Parameter find_last_opt : (elt -> bool) -> t -> option elt.

    Parameter of_list : list elt -> t.

    Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

    Parameter to_seq : t -> OCaml.Seq.t elt.

    Parameter add_seq : OCaml.Seq.t elt -> t -> t.

    Parameter of_seq : OCaml.Seq.t elt -> t.

    Parameter encoding : Data_encoding.t elt.
  End __Set.

  Module Map.
    Definition key := t.

    Parameter t : forall (a : Set), Set.

    Parameter empty : forall {a : Set}, t a.

    Parameter is_empty : forall {a : Set}, t a -> bool.

    Parameter mem : forall {a : Set}, key -> t a -> bool.

    Parameter add : forall {a : Set}, key -> a -> t a -> t a.

    Parameter update : forall {a : Set},
      key -> (option a -> option a) -> t a -> t a.

    Parameter singleton : forall {a : Set}, key -> a -> t a.

    Parameter remove : forall {a : Set}, key -> t a -> t a.

    Parameter merge : forall {a b c : Set},
      (key -> option a -> option b -> option c) -> t a -> t b -> t c.

    Parameter union : forall {a : Set},
      (key -> a -> a -> option a) -> t a -> t a -> t a.

    Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

    Parameter equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool.

    Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

    Parameter fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b.

    Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

    Parameter partition : forall {a : Set},
      (key -> a -> bool) -> t a -> t a * t a.

    Parameter cardinal : forall {a : Set}, t a -> Z.

    Parameter bindings : forall {a : Set}, t a -> list (key * a).

    Parameter min_binding : forall {a : Set}, t a -> key * a.

    Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter max_binding : forall {a : Set}, t a -> key * a.

    Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter choose : forall {a : Set}, t a -> key * a.

    Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

    Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

    Parameter find : forall {a : Set}, key -> t a -> a.

    Parameter find_opt : forall {a : Set}, key -> t a -> option a.

    Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_first_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_last_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

    Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

    Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

    Parameter to_seq_from : forall {a : Set},
      key -> t a -> OCaml.Seq.t (key * a).

    Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

    Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

    Parameter encoding : forall {a : Set},
      Data_encoding.t a -> Data_encoding.t (t a).
  End Map.
End Operation_hash.

Module Operation_list_hash.
  Definition elt := Operation_hash.t.

  Parameter t : Set.

  Parameter name : string.

  Parameter title : string.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter pp_short : Format.formatter -> t -> unit.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter hash_bytes : option MBytes.t -> list MBytes.t -> t.

  Parameter hash_string : option string -> list string -> t.

  Parameter zero : t.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter to_path : t -> list string -> list string.

  Parameter of_path : list string -> option t.

  Parameter of_path_exn : list string -> t.

  Parameter prefix_path : string -> list string.

  Parameter path_length : Z.

  Module __Set.
    Definition elt := t.

    Parameter t : Set.

    Parameter empty : t.

    Parameter is_empty : t -> bool.

    Parameter mem : elt -> t -> bool.

    Parameter add : elt -> t -> t.

    Parameter singleton : elt -> t.

    Parameter remove : elt -> t -> t.

    Parameter union : t -> t -> t.

    Parameter inter : t -> t -> t.

    Parameter diff : t -> t -> t.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter subset : t -> t -> bool.

    Parameter iter : (elt -> unit) -> t -> unit.

    Parameter map : (elt -> elt) -> t -> t.

    Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

    Parameter for_all : (elt -> bool) -> t -> bool.

    Parameter __exists : (elt -> bool) -> t -> bool.

    Parameter filter : (elt -> bool) -> t -> t.

    Parameter partition : (elt -> bool) -> t -> t * t.

    Parameter cardinal : t -> Z.

    Parameter elements : t -> list elt.

    Parameter min_elt : t -> elt.

    Parameter min_elt_opt : t -> option elt.

    Parameter max_elt : t -> elt.

    Parameter max_elt_opt : t -> option elt.

    Parameter choose : t -> elt.

    Parameter choose_opt : t -> option elt.

    Parameter split : elt -> t -> t * bool * t.

    Parameter find : elt -> t -> elt.

    Parameter find_opt : elt -> t -> option elt.

    Parameter find_first : (elt -> bool) -> t -> elt.

    Parameter find_first_opt : (elt -> bool) -> t -> option elt.

    Parameter find_last : (elt -> bool) -> t -> elt.

    Parameter find_last_opt : (elt -> bool) -> t -> option elt.

    Parameter of_list : list elt -> t.

    Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

    Parameter to_seq : t -> OCaml.Seq.t elt.

    Parameter add_seq : OCaml.Seq.t elt -> t -> t.

    Parameter of_seq : OCaml.Seq.t elt -> t.

    Parameter encoding : Data_encoding.t elt.
  End __Set.

  Module Map.
    Definition key := t.

    Parameter t : forall (a : Set), Set.

    Parameter empty : forall {a : Set}, t a.

    Parameter is_empty : forall {a : Set}, t a -> bool.

    Parameter mem : forall {a : Set}, key -> t a -> bool.

    Parameter add : forall {a : Set}, key -> a -> t a -> t a.

    Parameter update : forall {a : Set},
      key -> (option a -> option a) -> t a -> t a.

    Parameter singleton : forall {a : Set}, key -> a -> t a.

    Parameter remove : forall {a : Set}, key -> t a -> t a.

    Parameter merge : forall {a b c : Set},
      (key -> option a -> option b -> option c) -> t a -> t b -> t c.

    Parameter union : forall {a : Set},
      (key -> a -> a -> option a) -> t a -> t a -> t a.

    Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

    Parameter equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool.

    Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

    Parameter fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b.

    Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

    Parameter partition : forall {a : Set},
      (key -> a -> bool) -> t a -> t a * t a.

    Parameter cardinal : forall {a : Set}, t a -> Z.

    Parameter bindings : forall {a : Set}, t a -> list (key * a).

    Parameter min_binding : forall {a : Set}, t a -> key * a.

    Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter max_binding : forall {a : Set}, t a -> key * a.

    Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter choose : forall {a : Set}, t a -> key * a.

    Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

    Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

    Parameter find : forall {a : Set}, key -> t a -> a.

    Parameter find_opt : forall {a : Set}, key -> t a -> option a.

    Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_first_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_last_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

    Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

    Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

    Parameter to_seq_from : forall {a : Set},
      key -> t a -> OCaml.Seq.t (key * a).

    Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

    Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

    Parameter encoding : forall {a : Set},
      Data_encoding.t a -> Data_encoding.t (t a).
  End Map.

  Parameter compute : list elt -> t.

  Parameter empty : t.

  Parameter path : Set.

  Parameter compute_path : list elt -> Z -> path.

  Parameter check_path : path -> elt -> t * Z.

  Parameter path_encoding : Data_encoding.t path.
End Operation_list_hash.

Module Operation_list_list_hash.
  Definition elt := Operation_list_hash.t.

  Parameter t : Set.

  Parameter name : string.

  Parameter title : string.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter pp_short : Format.formatter -> t -> unit.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter hash_bytes : option MBytes.t -> list MBytes.t -> t.

  Parameter hash_string : option string -> list string -> t.

  Parameter zero : t.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter to_path : t -> list string -> list string.

  Parameter of_path : list string -> option t.

  Parameter of_path_exn : list string -> t.

  Parameter prefix_path : string -> list string.

  Parameter path_length : Z.

  Module __Set.
    Definition elt := t.

    Parameter t : Set.

    Parameter empty : t.

    Parameter is_empty : t -> bool.

    Parameter mem : elt -> t -> bool.

    Parameter add : elt -> t -> t.

    Parameter singleton : elt -> t.

    Parameter remove : elt -> t -> t.

    Parameter union : t -> t -> t.

    Parameter inter : t -> t -> t.

    Parameter diff : t -> t -> t.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter subset : t -> t -> bool.

    Parameter iter : (elt -> unit) -> t -> unit.

    Parameter map : (elt -> elt) -> t -> t.

    Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

    Parameter for_all : (elt -> bool) -> t -> bool.

    Parameter __exists : (elt -> bool) -> t -> bool.

    Parameter filter : (elt -> bool) -> t -> t.

    Parameter partition : (elt -> bool) -> t -> t * t.

    Parameter cardinal : t -> Z.

    Parameter elements : t -> list elt.

    Parameter min_elt : t -> elt.

    Parameter min_elt_opt : t -> option elt.

    Parameter max_elt : t -> elt.

    Parameter max_elt_opt : t -> option elt.

    Parameter choose : t -> elt.

    Parameter choose_opt : t -> option elt.

    Parameter split : elt -> t -> t * bool * t.

    Parameter find : elt -> t -> elt.

    Parameter find_opt : elt -> t -> option elt.

    Parameter find_first : (elt -> bool) -> t -> elt.

    Parameter find_first_opt : (elt -> bool) -> t -> option elt.

    Parameter find_last : (elt -> bool) -> t -> elt.

    Parameter find_last_opt : (elt -> bool) -> t -> option elt.

    Parameter of_list : list elt -> t.

    Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

    Parameter to_seq : t -> OCaml.Seq.t elt.

    Parameter add_seq : OCaml.Seq.t elt -> t -> t.

    Parameter of_seq : OCaml.Seq.t elt -> t.

    Parameter encoding : Data_encoding.t elt.
  End __Set.

  Module Map.
    Definition key := t.

    Parameter t : forall (a : Set), Set.

    Parameter empty : forall {a : Set}, t a.

    Parameter is_empty : forall {a : Set}, t a -> bool.

    Parameter mem : forall {a : Set}, key -> t a -> bool.

    Parameter add : forall {a : Set}, key -> a -> t a -> t a.

    Parameter update : forall {a : Set},
      key -> (option a -> option a) -> t a -> t a.

    Parameter singleton : forall {a : Set}, key -> a -> t a.

    Parameter remove : forall {a : Set}, key -> t a -> t a.

    Parameter merge : forall {a b c : Set},
      (key -> option a -> option b -> option c) -> t a -> t b -> t c.

    Parameter union : forall {a : Set},
      (key -> a -> a -> option a) -> t a -> t a -> t a.

    Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

    Parameter equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool.

    Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

    Parameter fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b.

    Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

    Parameter partition : forall {a : Set},
      (key -> a -> bool) -> t a -> t a * t a.

    Parameter cardinal : forall {a : Set}, t a -> Z.

    Parameter bindings : forall {a : Set}, t a -> list (key * a).

    Parameter min_binding : forall {a : Set}, t a -> key * a.

    Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter max_binding : forall {a : Set}, t a -> key * a.

    Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter choose : forall {a : Set}, t a -> key * a.

    Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

    Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

    Parameter find : forall {a : Set}, key -> t a -> a.

    Parameter find_opt : forall {a : Set}, key -> t a -> option a.

    Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_first_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_last_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

    Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

    Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

    Parameter to_seq_from : forall {a : Set},
      key -> t a -> OCaml.Seq.t (key * a).

    Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

    Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

    Parameter encoding : forall {a : Set},
      Data_encoding.t a -> Data_encoding.t (t a).
  End Map.

  Parameter compute : list elt -> t.

  Parameter empty : t.

  Parameter path : Set.

  Parameter compute_path : list elt -> Z -> path.

  Parameter check_path : path -> elt -> t * Z.

  Parameter path_encoding : Data_encoding.t path.
End Operation_list_list_hash.

Module Protocol_hash.
  Parameter t : Set.

  Parameter name : string.

  Parameter title : string.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter pp_short : Format.formatter -> t -> unit.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter hash_bytes : option MBytes.t -> list MBytes.t -> t.

  Parameter hash_string : option string -> list string -> t.

  Parameter zero : t.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter to_path : t -> list string -> list string.

  Parameter of_path : list string -> option t.

  Parameter of_path_exn : list string -> t.

  Parameter prefix_path : string -> list string.

  Parameter path_length : Z.

  Module __Set.
    Definition elt := t.

    Parameter t : Set.

    Parameter empty : t.

    Parameter is_empty : t -> bool.

    Parameter mem : elt -> t -> bool.

    Parameter add : elt -> t -> t.

    Parameter singleton : elt -> t.

    Parameter remove : elt -> t -> t.

    Parameter union : t -> t -> t.

    Parameter inter : t -> t -> t.

    Parameter diff : t -> t -> t.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter subset : t -> t -> bool.

    Parameter iter : (elt -> unit) -> t -> unit.

    Parameter map : (elt -> elt) -> t -> t.

    Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

    Parameter for_all : (elt -> bool) -> t -> bool.

    Parameter __exists : (elt -> bool) -> t -> bool.

    Parameter filter : (elt -> bool) -> t -> t.

    Parameter partition : (elt -> bool) -> t -> t * t.

    Parameter cardinal : t -> Z.

    Parameter elements : t -> list elt.

    Parameter min_elt : t -> elt.

    Parameter min_elt_opt : t -> option elt.

    Parameter max_elt : t -> elt.

    Parameter max_elt_opt : t -> option elt.

    Parameter choose : t -> elt.

    Parameter choose_opt : t -> option elt.

    Parameter split : elt -> t -> t * bool * t.

    Parameter find : elt -> t -> elt.

    Parameter find_opt : elt -> t -> option elt.

    Parameter find_first : (elt -> bool) -> t -> elt.

    Parameter find_first_opt : (elt -> bool) -> t -> option elt.

    Parameter find_last : (elt -> bool) -> t -> elt.

    Parameter find_last_opt : (elt -> bool) -> t -> option elt.

    Parameter of_list : list elt -> t.

    Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

    Parameter to_seq : t -> OCaml.Seq.t elt.

    Parameter add_seq : OCaml.Seq.t elt -> t -> t.

    Parameter of_seq : OCaml.Seq.t elt -> t.

    Parameter encoding : Data_encoding.t elt.
  End __Set.

  Module Map.
    Definition key := t.

    Parameter t : forall (a : Set), Set.

    Parameter empty : forall {a : Set}, t a.

    Parameter is_empty : forall {a : Set}, t a -> bool.

    Parameter mem : forall {a : Set}, key -> t a -> bool.

    Parameter add : forall {a : Set}, key -> a -> t a -> t a.

    Parameter update : forall {a : Set},
      key -> (option a -> option a) -> t a -> t a.

    Parameter singleton : forall {a : Set}, key -> a -> t a.

    Parameter remove : forall {a : Set}, key -> t a -> t a.

    Parameter merge : forall {a b c : Set},
      (key -> option a -> option b -> option c) -> t a -> t b -> t c.

    Parameter union : forall {a : Set},
      (key -> a -> a -> option a) -> t a -> t a -> t a.

    Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

    Parameter equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool.

    Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

    Parameter fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b.

    Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

    Parameter partition : forall {a : Set},
      (key -> a -> bool) -> t a -> t a * t a.

    Parameter cardinal : forall {a : Set}, t a -> Z.

    Parameter bindings : forall {a : Set}, t a -> list (key * a).

    Parameter min_binding : forall {a : Set}, t a -> key * a.

    Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter max_binding : forall {a : Set}, t a -> key * a.

    Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter choose : forall {a : Set}, t a -> key * a.

    Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

    Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

    Parameter find : forall {a : Set}, key -> t a -> a.

    Parameter find_opt : forall {a : Set}, key -> t a -> option a.

    Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_first_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_last_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

    Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

    Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

    Parameter to_seq_from : forall {a : Set},
      key -> t a -> OCaml.Seq.t (key * a).

    Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

    Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

    Parameter encoding : forall {a : Set},
      Data_encoding.t a -> Data_encoding.t (t a).
  End Map.
End Protocol_hash.

Module Context_hash.
  Parameter t : Set.

  Parameter name : string.

  Parameter title : string.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter pp_short : Format.formatter -> t -> unit.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter hash_bytes : option MBytes.t -> list MBytes.t -> t.

  Parameter hash_string : option string -> list string -> t.

  Parameter zero : t.

  Parameter size : Z.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes_opt : MBytes.t -> option t.

  Parameter of_bytes_exn : MBytes.t -> t.

  Parameter to_b58check : t -> string.

  Parameter to_short_b58check : t -> string.

  Parameter of_b58check_exn : string -> t.

  Parameter of_b58check_opt : string -> option t.

  (* extensible_type Base58.data *)

  Parameter b58check_encoding : Base58.encoding t.

  Parameter encoding : Data_encoding.t t.

  Parameter rpc_arg : RPC_arg.t t.

  Parameter to_path : t -> list string -> list string.

  Parameter of_path : list string -> option t.

  Parameter of_path_exn : list string -> t.

  Parameter prefix_path : string -> list string.

  Parameter path_length : Z.

  Module __Set.
    Definition elt := t.

    Parameter t : Set.

    Parameter empty : t.

    Parameter is_empty : t -> bool.

    Parameter mem : elt -> t -> bool.

    Parameter add : elt -> t -> t.

    Parameter singleton : elt -> t.

    Parameter remove : elt -> t -> t.

    Parameter union : t -> t -> t.

    Parameter inter : t -> t -> t.

    Parameter diff : t -> t -> t.

    Parameter compare : t -> t -> Z.

    Parameter equal : t -> t -> bool.

    Parameter subset : t -> t -> bool.

    Parameter iter : (elt -> unit) -> t -> unit.

    Parameter map : (elt -> elt) -> t -> t.

    Parameter fold : forall {a : Set}, (elt -> a -> a) -> t -> a -> a.

    Parameter for_all : (elt -> bool) -> t -> bool.

    Parameter __exists : (elt -> bool) -> t -> bool.

    Parameter filter : (elt -> bool) -> t -> t.

    Parameter partition : (elt -> bool) -> t -> t * t.

    Parameter cardinal : t -> Z.

    Parameter elements : t -> list elt.

    Parameter min_elt : t -> elt.

    Parameter min_elt_opt : t -> option elt.

    Parameter max_elt : t -> elt.

    Parameter max_elt_opt : t -> option elt.

    Parameter choose : t -> elt.

    Parameter choose_opt : t -> option elt.

    Parameter split : elt -> t -> t * bool * t.

    Parameter find : elt -> t -> elt.

    Parameter find_opt : elt -> t -> option elt.

    Parameter find_first : (elt -> bool) -> t -> elt.

    Parameter find_first_opt : (elt -> bool) -> t -> option elt.

    Parameter find_last : (elt -> bool) -> t -> elt.

    Parameter find_last_opt : (elt -> bool) -> t -> option elt.

    Parameter of_list : list elt -> t.

    Parameter to_seq_from : elt -> t -> OCaml.Seq.t elt.

    Parameter to_seq : t -> OCaml.Seq.t elt.

    Parameter add_seq : OCaml.Seq.t elt -> t -> t.

    Parameter of_seq : OCaml.Seq.t elt -> t.

    Parameter encoding : Data_encoding.t elt.
  End __Set.

  Module Map.
    Definition key := t.

    Parameter t : forall (a : Set), Set.

    Parameter empty : forall {a : Set}, t a.

    Parameter is_empty : forall {a : Set}, t a -> bool.

    Parameter mem : forall {a : Set}, key -> t a -> bool.

    Parameter add : forall {a : Set}, key -> a -> t a -> t a.

    Parameter update : forall {a : Set},
      key -> (option a -> option a) -> t a -> t a.

    Parameter singleton : forall {a : Set}, key -> a -> t a.

    Parameter remove : forall {a : Set}, key -> t a -> t a.

    Parameter merge : forall {a b c : Set},
      (key -> option a -> option b -> option c) -> t a -> t b -> t c.

    Parameter union : forall {a : Set},
      (key -> a -> a -> option a) -> t a -> t a -> t a.

    Parameter compare : forall {a : Set}, (a -> a -> Z) -> t a -> t a -> Z.

    Parameter equal : forall {a : Set}, (a -> a -> bool) -> t a -> t a -> bool.

    Parameter iter : forall {a : Set}, (key -> a -> unit) -> t a -> unit.

    Parameter fold : forall {a b : Set}, (key -> a -> b -> b) -> t a -> b -> b.

    Parameter for_all : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter __exists : forall {a : Set}, (key -> a -> bool) -> t a -> bool.

    Parameter filter : forall {a : Set}, (key -> a -> bool) -> t a -> t a.

    Parameter partition : forall {a : Set},
      (key -> a -> bool) -> t a -> t a * t a.

    Parameter cardinal : forall {a : Set}, t a -> Z.

    Parameter bindings : forall {a : Set}, t a -> list (key * a).

    Parameter min_binding : forall {a : Set}, t a -> key * a.

    Parameter min_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter max_binding : forall {a : Set}, t a -> key * a.

    Parameter max_binding_opt : forall {a : Set}, t a -> option (key * a).

    Parameter choose : forall {a : Set}, t a -> key * a.

    Parameter choose_opt : forall {a : Set}, t a -> option (key * a).

    Parameter split : forall {a : Set}, key -> t a -> t a * option a * t a.

    Parameter find : forall {a : Set}, key -> t a -> a.

    Parameter find_opt : forall {a : Set}, key -> t a -> option a.

    Parameter find_first : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_first_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter find_last : forall {a : Set}, (key -> bool) -> t a -> key * a.

    Parameter find_last_opt : forall {a : Set},
      (key -> bool) -> t a -> option (key * a).

    Parameter map : forall {a b : Set}, (a -> b) -> t a -> t b.

    Parameter mapi : forall {a b : Set}, (key -> a -> b) -> t a -> t b.

    Parameter to_seq : forall {a : Set}, t a -> OCaml.Seq.t (key * a).

    Parameter to_seq_from : forall {a : Set},
      key -> t a -> OCaml.Seq.t (key * a).

    Parameter add_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a -> t a.

    Parameter of_seq : forall {a : Set}, OCaml.Seq.t (key * a) -> t a.

    Parameter encoding : forall {a : Set},
      Data_encoding.t a -> Data_encoding.t (t a).
  End Map.
End Context_hash.

Module Micheline.
  Definition annot := list string.

  Inductive node (l p : Set) : Set :=
  | Int : l -> Z.t -> node l p
  | String : l -> string -> node l p
  | Bytes : l -> MBytes.t -> node l p
  | Prim : l -> p -> list (node l p) -> annot -> node l p
  | Seq : l -> list (node l p) -> node l p.

  Arguments Int {_ _}.
  Arguments String {_ _}.
  Arguments Bytes {_ _}.
  Arguments Prim {_ _}.
  Arguments Seq {_ _}.

  Parameter canonical : forall (p : Set), Set.

  Definition canonical_location := Z.

  Parameter root : forall {p : Set}, canonical p -> node canonical_location p.

  Parameter canonical_location_encoding :
    Data_encoding.encoding canonical_location.

  Parameter canonical_encoding : forall {l : Set},
    string -> Data_encoding.encoding l -> Data_encoding.encoding (canonical l).

  Parameter canonical_encoding_v1 : forall {l : Set},
    string -> Data_encoding.encoding l -> Data_encoding.encoding (canonical l).

  Parameter location : forall {l p : Set}, node l p -> l.

  Parameter annotations : forall {l p : Set}, node l p -> list string.

  Parameter strip_locations : forall {A p : Set}, node A p -> canonical p.

  Parameter extract_locations : forall {l p : Set},
    node l p -> canonical p * list (canonical_location * l).

  Parameter inject_locations : forall {l p : Set},
    (canonical_location -> l) -> canonical p -> node l p.
End Micheline.

Module Block_header.
  Module shell_header.
    Record record := {
      level : Int32.t;
      proto_level : Z;
      predecessor : Block_hash.t;
      timestamp : Time.t;
      validation_passes : Z;
      operations_hash : Operation_list_list_hash.t;
      fitness : list MBytes.t;
      context : Context_hash.t }.
  End shell_header.
  Definition shell_header := shell_header.record.

  Parameter shell_header_encoding : Data_encoding.t shell_header.

  Module t.
    Record record := {
      shell : shell_header;
      protocol_data : MBytes.t }.
  End t.
  Definition t := t.record.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter encoding : Data_encoding.t t.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes : MBytes.t -> option t.

  Parameter __hash_value : t -> Block_hash.t.

  Parameter hash_raw : MBytes.t -> Block_hash.t.
End Block_header.

Module Fitness.
  Definition t := list MBytes.t.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter encoding : Data_encoding.t t.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes : MBytes.t -> option t.
End Fitness.

Module Operation.
  Module shell_header.
    Record record := {
      branch : Block_hash.t }.
  End shell_header.
  Definition shell_header := shell_header.record.

  Parameter shell_header_encoding : Data_encoding.t shell_header.

  Module t.
    Record record := {
      shell : shell_header;
      proto : MBytes.t }.
  End t.
  Definition t := t.record.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter encoding : Data_encoding.t t.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes : MBytes.t -> option t.

  Parameter __hash_value : t -> Operation_hash.t.

  Parameter hash_raw : MBytes.t -> Operation_hash.t.
End Operation.

Module Protocol.
  Reserved Notation "'component".
  Reserved Notation "'t".

  Module t_skeleton.
    Record record {expected_env components : Set} := {
      expected_env : expected_env;
      components : components }.
    Arguments record : clear implicits.
  End t_skeleton.
  Definition t_skeleton := t_skeleton.record.

  Module component_skeleton.
    Record record {name interface implementation : Set} := {
      name : name;
      interface : interface;
      implementation : implementation }.
    Arguments record : clear implicits.
  End component_skeleton.
  Definition component_skeleton := component_skeleton.record.

  Inductive env_version : Set :=
  | V1 : env_version
  
  where "'component" := (component_skeleton string (option string) string)
  and "'t" := (t_skeleton env_version (list 'component)).

  Definition component := 'component.
  Definition t := 't.

  Parameter component_encoding : Data_encoding.t component.

  Parameter env_version_encoding : Data_encoding.t env_version.

  Parameter op_eq : t -> t -> bool.

  Parameter op_ltgt : t -> t -> bool.

  Parameter op_lt : t -> t -> bool.

  Parameter op_lteq : t -> t -> bool.

  Parameter op_gteq : t -> t -> bool.

  Parameter op_gt : t -> t -> bool.

  Parameter compare : t -> t -> Z.

  Parameter equal : t -> t -> bool.

  Parameter max : t -> t -> t.

  Parameter min : t -> t -> t.

  Parameter pp : Format.formatter -> t -> unit.

  Parameter encoding : Data_encoding.t t.

  Parameter to_bytes : t -> MBytes.t.

  Parameter of_bytes : MBytes.t -> option t.

  Parameter __hash_value : t -> Protocol_hash.t.

  Parameter hash_raw : MBytes.t -> Protocol_hash.t.
End Protocol.

Module Context.
  Parameter t : Set.

  Definition key := list string.

  Definition value := MBytes.t.

  Parameter mem : t -> key -> Lwt.t bool.

  Parameter dir_mem : t -> key -> Lwt.t bool.

  Parameter get : t -> key -> Lwt.t (option value).

  Parameter set : t -> key -> value -> Lwt.t t.

  Parameter copy : t -> key -> key -> Lwt.t (option t).

  Parameter del : t -> key -> Lwt.t t.

  Parameter remove_rec : t -> key -> Lwt.t t.

  Parameter fold : forall {a : Set},
    t -> key -> a -> ((* `Dir *) key + (* `Key *) key -> a -> Lwt.t a) ->
    Lwt.t a.

  Parameter keys : t -> key -> Lwt.t (list key).

  Parameter fold_keys : forall {a : Set},
    t -> key -> a -> (key -> a -> Lwt.t a) -> Lwt.t a.

  Parameter register_resolver : forall {a : Set},
    Base58.encoding a -> (t -> string -> Lwt.t (list a)) -> unit.

  Parameter complete : t -> string -> Lwt.t (list string).
End Context.

Module Updater.
  Module validation_result.
    Record record := {
      context : Context.t;
      fitness : Fitness.t;
      message : option string;
      max_operations_ttl : Z;
      last_allowed_fork_level : Int32.t }.
  End validation_result.
  Definition validation_result := validation_result.record.

  Module quota.
    Record record := {
      max_size : Z;
      max_op : option Z }.
  End quota.
  Definition quota := quota.record.

  Module rpc_context.
    Record record := {
      block_hash : Block_hash.t;
      block_header : Block_header.shell_header;
      context : Context.t }.
  End rpc_context.
  Definition rpc_context := rpc_context.record.

  Module PROTOCOL.
    Record signature {block_header_data block_header block_header_metadata
      operation_data operation_receipt operation validation_state : Set} := {
      max_block_length : Z;
      max_operation_data_length : Z;
      validation_passes : list quota;
      block_header_data := block_header_data;
      block_header_data_encoding : Data_encoding.t block_header_data;
      block_header := block_header;
      block_header_metadata := block_header_metadata;
      block_header_metadata_encoding : Data_encoding.t block_header_metadata;
      operation_data := operation_data;
      operation_receipt := operation_receipt;
      operation := operation;
      operation_data_encoding : Data_encoding.t operation_data;
      operation_receipt_encoding : Data_encoding.t operation_receipt;
      operation_data_and_receipt_encoding :
        Data_encoding.t (operation_data * operation_receipt);
      acceptable_passes : operation -> list Z;
      compare_operations : operation -> operation -> Z;
      validation_state := validation_state;
      current_context :
        validation_state -> Lwt.t (Error_monad.tzresult Context.t);
      begin_partial_application :
        Chain_id.t -> Context.t -> Time.t -> Fitness.t -> block_header ->
        Lwt.t (Error_monad.tzresult validation_state);
      begin_application :
        Chain_id.t -> Context.t -> Time.t -> Fitness.t -> block_header ->
        Lwt.t (Error_monad.tzresult validation_state);
      begin_construction :
        Chain_id.t -> Context.t -> Time.t -> Int32.t -> Fitness.t ->
        Block_hash.t -> Time.t -> option block_header_data -> unit ->
        Lwt.t (Error_monad.tzresult validation_state);
      apply_operation :
        validation_state -> operation ->
        Lwt.t (Error_monad.tzresult (validation_state * operation_receipt));
      finalize_block :
        validation_state ->
        Lwt.t (Error_monad.tzresult (validation_result * block_header_metadata));
      rpc_services : RPC_directory.t rpc_context;
      init :
        Context.t -> Block_header.shell_header ->
        Lwt.t (Error_monad.tzresult validation_result);
    }.
    Arguments signature : clear implicits.
  End PROTOCOL.

  Parameter activate : Context.t -> Protocol_hash.t -> Lwt.t Context.t.

  Parameter fork_test_chain :
    Context.t -> Protocol_hash.t -> Time.t -> Lwt.t Context.t.
End Updater.

Module RPC_context.
  Definition t := Updater.rpc_context.

  (* class_type *)

  Parameter make_call0 : forall {E G I K L a b c i o pr q : Set},
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o ->
    (((RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o)) * (E * q * i * o)) *
      (((RPC_service.t
        ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
          (* `POST *) unit + (* `PATCH *) unit) t (t * a) q i o -> pr -> a ->
      q -> i -> Lwt.t (Error_monad.shell_tzresult o)) * (G * a * q * i * o)) *
        (((RPC_service.t
          ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
            (* `POST *) unit + (* `PATCH *) unit) t ((t * a) * b) q i o -> pr ->
        a -> b -> q -> i -> Lwt.t (Error_monad.shell_tzresult o)) *
          (I * a * b * q * i * o)) *
          (((RPC_service.t
            ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
              (* `POST *) unit + (* `PATCH *) unit) t (((t * a) * b) * c) q i o
          -> pr -> a -> b -> c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o))
            * (K * a * b * c * q * i * o)) * L)))) * L * pr -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o).

  Parameter make_call1 : forall {F G I K L a b c i o pr q : Set},
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t (t * a) q i o ->
    (((RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o)) * (F * q * i * o)) *
      (((RPC_service.t
        ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
          (* `POST *) unit + (* `PATCH *) unit) t (t * a) q i o -> pr -> a ->
      q -> i -> Lwt.t (Error_monad.shell_tzresult o)) * (G * a * q * i * o)) *
        (((RPC_service.t
          ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
            (* `POST *) unit + (* `PATCH *) unit) t ((t * a) * b) q i o -> pr ->
        a -> b -> q -> i -> Lwt.t (Error_monad.shell_tzresult o)) *
          (I * a * b * q * i * o)) *
          (((RPC_service.t
            ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
              (* `POST *) unit + (* `PATCH *) unit) t (((t * a) * b) * c) q i o
          -> pr -> a -> b -> c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o))
            * (K * a * b * c * q * i * o)) * L)))) * L * pr -> pr -> a -> q ->
    i -> Lwt.t (Error_monad.shell_tzresult o).

  Parameter make_call2 : forall {G H I K L a b c i o pr q : Set},
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t ((t * a) * b) q i o ->
    (((RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o)) * (G * q * i * o)) *
      (((RPC_service.t
        ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
          (* `POST *) unit + (* `PATCH *) unit) t (t * a) q i o -> pr -> a ->
      q -> i -> Lwt.t (Error_monad.shell_tzresult o)) * (H * a * q * i * o)) *
        (((RPC_service.t
          ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
            (* `POST *) unit + (* `PATCH *) unit) t ((t * a) * b) q i o -> pr ->
        a -> b -> q -> i -> Lwt.t (Error_monad.shell_tzresult o)) *
          (I * a * b * q * i * o)) *
          (((RPC_service.t
            ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
              (* `POST *) unit + (* `PATCH *) unit) t (((t * a) * b) * c) q i o
          -> pr -> a -> b -> c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o))
            * (K * a * b * c * q * i * o)) * L)))) * L * pr -> pr -> a -> b ->
    q -> i -> Lwt.t (Error_monad.shell_tzresult o).

  Parameter make_call3 : forall {H I J K L a b c i o pr q : Set},
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t (((t * a) * b) * c) q i o ->
    (((RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o)) * (H * q * i * o)) *
      (((RPC_service.t
        ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
          (* `POST *) unit + (* `PATCH *) unit) t (t * a) q i o -> pr -> a ->
      q -> i -> Lwt.t (Error_monad.shell_tzresult o)) * (I * a * q * i * o)) *
        (((RPC_service.t
          ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
            (* `POST *) unit + (* `PATCH *) unit) t ((t * a) * b) q i o -> pr ->
        a -> b -> q -> i -> Lwt.t (Error_monad.shell_tzresult o)) *
          (J * a * b * q * i * o)) *
          (((RPC_service.t
            ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
              (* `POST *) unit + (* `PATCH *) unit) t (((t * a) * b) * c) q i o
          -> pr -> a -> b -> c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o))
            * (K * a * b * c * q * i * o)) * L)))) * L * pr -> pr -> a -> b ->
    c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o).

  Parameter make_opt_call0 : forall {E G I K L a b c i o pr q : Set},
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o ->
    (((RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o)) * (E * q * i * o)) *
      (((RPC_service.t
        ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
          (* `POST *) unit + (* `PATCH *) unit) t (t * a) q i o -> pr -> a ->
      q -> i -> Lwt.t (Error_monad.shell_tzresult o)) * (G * a * q * i * o)) *
        (((RPC_service.t
          ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
            (* `POST *) unit + (* `PATCH *) unit) t ((t * a) * b) q i o -> pr ->
        a -> b -> q -> i -> Lwt.t (Error_monad.shell_tzresult o)) *
          (I * a * b * q * i * o)) *
          (((RPC_service.t
            ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
              (* `POST *) unit + (* `PATCH *) unit) t (((t * a) * b) * c) q i o
          -> pr -> a -> b -> c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o))
            * (K * a * b * c * q * i * o)) * L)))) * L * pr -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult (option o)).

  Parameter make_opt_call1 : forall {F G I K L a b c i o pr q : Set},
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t (t * a) q i o ->
    (((RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o)) * (F * q * i * o)) *
      (((RPC_service.t
        ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
          (* `POST *) unit + (* `PATCH *) unit) t (t * a) q i o -> pr -> a ->
      q -> i -> Lwt.t (Error_monad.shell_tzresult o)) * (G * a * q * i * o)) *
        (((RPC_service.t
          ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
            (* `POST *) unit + (* `PATCH *) unit) t ((t * a) * b) q i o -> pr ->
        a -> b -> q -> i -> Lwt.t (Error_monad.shell_tzresult o)) *
          (I * a * b * q * i * o)) *
          (((RPC_service.t
            ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
              (* `POST *) unit + (* `PATCH *) unit) t (((t * a) * b) * c) q i o
          -> pr -> a -> b -> c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o))
            * (K * a * b * c * q * i * o)) * L)))) * L * pr -> pr -> a -> q ->
    i -> Lwt.t (Error_monad.shell_tzresult (option o)).

  Parameter make_opt_call2 : forall {G H I K L a b c i o pr q : Set},
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t ((t * a) * b) q i o ->
    (((RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o)) * (G * q * i * o)) *
      (((RPC_service.t
        ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
          (* `POST *) unit + (* `PATCH *) unit) t (t * a) q i o -> pr -> a ->
      q -> i -> Lwt.t (Error_monad.shell_tzresult o)) * (H * a * q * i * o)) *
        (((RPC_service.t
          ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
            (* `POST *) unit + (* `PATCH *) unit) t ((t * a) * b) q i o -> pr ->
        a -> b -> q -> i -> Lwt.t (Error_monad.shell_tzresult o)) *
          (I * a * b * q * i * o)) *
          (((RPC_service.t
            ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
              (* `POST *) unit + (* `PATCH *) unit) t (((t * a) * b) * c) q i o
          -> pr -> a -> b -> c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o))
            * (K * a * b * c * q * i * o)) * L)))) * L * pr -> pr -> a -> b ->
    q -> i -> Lwt.t (Error_monad.shell_tzresult (option o)).

  Parameter make_opt_call3 : forall {H I J K L a b c i o pr q : Set},
    RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t (((t * a) * b) * c) q i o ->
    (((RPC_service.t
      ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit + (* `POST *) unit
        + (* `PATCH *) unit) t t q i o -> pr -> q -> i ->
    Lwt.t (Error_monad.shell_tzresult o)) * (H * q * i * o)) *
      (((RPC_service.t
        ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
          (* `POST *) unit + (* `PATCH *) unit) t (t * a) q i o -> pr -> a ->
      q -> i -> Lwt.t (Error_monad.shell_tzresult o)) * (I * a * q * i * o)) *
        (((RPC_service.t
          ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
            (* `POST *) unit + (* `PATCH *) unit) t ((t * a) * b) q i o -> pr ->
        a -> b -> q -> i -> Lwt.t (Error_monad.shell_tzresult o)) *
          (J * a * b * q * i * o)) *
          (((RPC_service.t
            ((* `PUT *) unit + (* `GET *) unit + (* `DELETE *) unit +
              (* `POST *) unit + (* `PATCH *) unit) t (((t * a) * b) * c) q i o
          -> pr -> a -> b -> c -> q -> i -> Lwt.t (Error_monad.shell_tzresult o))
            * (K * a * b * c * q * i * o)) * L)))) * L * pr -> pr -> a -> b ->
    c -> q -> i -> Lwt.t (Error_monad.shell_tzresult (option o)).
End RPC_context.