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