🍃 V8_modules.v

Environment

Gitlab

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.Variant.

Module Type Pervasives_signature.
  Parameter raise : ∀ {a : Set}, extensible_type → a.

  Parameter raise_notrace : ∀ {a : Set}, extensible_type → a.

  Parameter invalid_arg : ∀ {a : Set}, string → a.

  Parameter failwith : ∀ {a : Set}, string → a.

  Parameter not : bool → bool.

  Parameter op_andand : bool → bool → bool.

  Parameter op_pipepipe : bool → bool → bool.

  Parameter __LOC__ : string.

  Parameter __FILE__ : string.

  Parameter __LINE__ : int.

  Parameter __MODULE__ : string.

  Parameter __POS__ : string × int × int × int.

  Parameter __LOC_OF__ : ∀ {a : Set}, a → string × a.

  Parameter __LINE_OF__ : ∀ {a : Set}, a → int × a.

  Parameter __POS_OF__ : ∀ {a : Set}, a → (string × int × int × int) × a.

  Parameter op_pipegt : ∀ {a b : Set}, a → (a → b) → b.

  Parameter op_atat : ∀ {a b : Set}, (a → b) → a → b.

  Parameter op_tildeminus : int → int.

  Parameter op_tildeplus : int → int.

  Parameter succ : int → int.

  Parameter pred : int → int.

  Parameter op_plus : int → int → int.

  Parameter op_minus : int → int → int.

  Parameter op_star : int → int → int.

  Parameter op_div : int → int → int.

  Parameter _mod : int → int → int.

  Parameter abs : int → int.

  Parameter max_int : int.

  Parameter min_int : int.

  Parameter land : int → int → int.

  Parameter lor : int → int → int.

  Parameter lxor : int → int → int.

  Parameter lnot : int → int.

  Parameter lsl : int → int → int.

  Parameter lsr : int → int → int.

  Parameter asr : int → int → int.

  Parameter op_caret : string → string → string.

  Parameter int_of_char : ascii → int.

  Parameter char_of_int : int → ascii.

  Parameter ignore : ∀ {a : Set}, a → unit.

  Parameter string_of_bool : bool → string.

  Parameter bool_of_string_opt : string → option bool.

  Parameter string_of_int : int → string.

  Parameter int_of_string_opt : string → option int.

  Parameter fst : ∀ {a b : Set}, a × b → a.

  Parameter snd : ∀ {a b : Set}, a × b → b.

  Parameter op_at : ∀ {a : Set}, list a → list a → list a.

  Module ref.
    Record record {a : Set} : Set := Build {
      contents : a;
    }.
    Arguments record : clear implicits.
    Definition with_contents {t_a} contents (r : record t_a) :=
      Build t_a contents.
  End ref.
  Definition ref := ref.record.

  Parameter ref_value : ∀ {a : Set}, a → ref a.

  Parameter op_exclamation : ∀ {a : Set}, ref a → a.

  Parameter op_coloneq : ∀ {a : Set}, ref a → a → unit.

  Parameter incr : ref int → unit.

  Parameter decr : ref int → 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) : Set :=
    CamlinternalFormatBasics.format6 a b c d e f.

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

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

  Parameter string_of_format : ∀ {a b c d e f : Set},
    format6 a b c d e f → string.

  Parameter format_of_string : ∀ {a b c d e f : Set},
    format6 a b c d e f → format6 a b c d e f.

  Parameter op_caretcaret : ∀ {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_signature.
Require Export TezosOfOCaml.Environment.V8.Pervasives.
Module Pervasives_check : Pervasives_signature := Pervasives.

Module Type Either_signature.
  Inductive t (a b : Set) : Set :=
  | Left : a → t a b
  | Right : b → t a b.

  Arguments Left {_ _}.
  Arguments Right {_ _}.

  Parameter equal : ∀ {a b : Set},
    (a → a → bool) → (b → b → bool) → t a b → t a b → bool.

  Parameter compare : ∀ {a b : Set},
    (a → a → int) → (b → b → int) → t a b → t a b → int.
End Either_signature.
Require Export TezosOfOCaml.Environment.V8.Either.
Module Either_check : Either_signature := Either.

Module Type String_signature.
  Parameter length : string → int.

  Parameter get : string → int → ascii.

  Parameter make : int → ascii → string.

  Parameter init_value : int → (int → ascii) → string.

  Parameter sub : string → int → int → string.

  Parameter blit : string → int → bytes → int → int → unit.

  Parameter concat : string → list string → string.

  Parameter iter : (ascii → unit) → string → unit.

  Parameter iteri : (int → ascii → unit) → string → unit.

  Parameter map : (ascii → ascii) → string → string.

  Parameter mapi : (int → ascii → ascii) → string → string.

  Parameter trim : string → string.

  Parameter escaped : string → string.

  Parameter index_opt : string → ascii → option int.

  Parameter rindex_opt : string → ascii → option int.

  Parameter index_from_opt : string → int → ascii → option int.

  Parameter rindex_from_opt : string → int → ascii → option int.

  Parameter contains : string → ascii → bool.

  Parameter contains_from : string → int → ascii → bool.

  Parameter rcontains_from : string → int → ascii → bool.

  Parameter uppercase_ascii : string → string.

  Parameter lowercase_ascii : string → string.

  Parameter capitalize_ascii : string → string.

  Parameter uncapitalize_ascii : string → string.

  Definition t : Set := string.

  Parameter compare : t → t → int.

  Parameter equal : t → t → bool.

  Parameter split_on_char : ascii → string → list string.
End String_signature.
Require Export TezosOfOCaml.Environment.V8.String.
Module String_check : String_signature := String.

Module Type Char_signature.
  Parameter code : ascii → int.

  Parameter chr : int → ascii.

  Parameter escaped : ascii → string.

  Parameter lowercase_ascii : ascii → ascii.

  Parameter uppercase_ascii : ascii → ascii.

  Definition t : Set := ascii.

  Parameter compare : t → t → int.

  Parameter equal : t → t → bool.
End Char_signature.
Require Export TezosOfOCaml.Environment.V8.Char.
Module Char_check : Char_signature := Char.

Module Type Bytes_signature.
  Parameter length : bytes → int.

  Parameter get : bytes → int → ascii.

  Parameter set : bytes → int → ascii → unit.

  Parameter make : int → ascii → bytes.

  Parameter init_value : int → (int → ascii) → bytes.

  Parameter empty : bytes.

  Parameter copy : bytes → bytes.

  Parameter of_string : string → bytes.

  Parameter to_string : bytes → string.

  Parameter sub : bytes → int → int → bytes.

  Parameter sub_string : bytes → int → int → string.

  Parameter extend : bytes → int → int → bytes.

  Parameter fill : bytes → int → int → ascii → unit.

  Parameter blit : bytes → int → bytes → int → int → unit.

  Parameter blit_string : string → int → bytes → int → int → unit.

  Parameter concat : bytes → list bytes → bytes.

  Parameter cat : bytes → bytes → bytes.

  Parameter iter : (ascii → unit) → bytes → unit.

  Parameter iteri : (int → ascii → unit) → bytes → unit.

  Parameter map : (ascii → ascii) → bytes → bytes.

  Parameter mapi : (int → ascii → ascii) → bytes → bytes.

  Parameter trim : bytes → bytes.

  Parameter escaped : bytes → bytes.

  Parameter index_opt : bytes → ascii → option int.

  Parameter rindex_opt : bytes → ascii → option int.

  Parameter index_from_opt : bytes → int → ascii → option int.

  Parameter rindex_from_opt : bytes → int → ascii → option int.

  Parameter contains : bytes → ascii → bool.

  Parameter contains_from : bytes → int → ascii → bool.

  Parameter rcontains_from : bytes → int → ascii → bool.

  Parameter uppercase_ascii : bytes → bytes.

  Parameter lowercase_ascii : bytes → bytes.

  Parameter capitalize_ascii : bytes → bytes.

  Parameter uncapitalize_ascii : bytes → bytes.

  Definition t : Set := bytes.

  Parameter compare : t → t → int.

  Parameter equal : t → t → bool.

  Parameter logand : bytes → bytes → bytes.

  Parameter logor : bytes → bytes → bytes.

  Parameter logxor : bytes → bytes → bytes.

  Parameter lognot : bytes → bytes.

  Parameter shift_left : bytes → int → bytes.

  Parameter shift_right : bytes → int → bytes.
End Bytes_signature.
Require Export TezosOfOCaml.Environment.V8.Bytes.
Module Bytes_check : Bytes_signature := Bytes.

Module Type Int32_signature.
  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 → int → int32.

  Parameter shift_right : int32 → int → int32.

  Parameter shift_right_logical : int32 → int → int32.

  Parameter of_int : int → int32.

  Parameter to_int : int32 → int.

  Parameter of_string_opt : string → option int32.

  Parameter to_string : int32 → string.

  Definition t : Set := int32.

  Parameter compare : t → t → int.

  Parameter equal : t → t → bool.
End Int32_signature.
Require Export TezosOfOCaml.Environment.V8.Int32.
Module Int32_check : Int32_signature := Int32.

Module Type Int64_signature.
  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 → int → int64.

  Parameter shift_right : int64 → int → int64.

  Parameter shift_right_logical : int64 → int → int64.

  Parameter of_int : int → int64.

  Parameter to_int : int64 → int.

  Parameter of_int32 : int32 → int64.

  Parameter to_int32 : int64 → int32.

  Parameter of_string_opt : string → option int64.

  Parameter to_string : int64 → string.

  Definition t : Set := int64.

  Parameter compare : t → t → int.

  Parameter equal : t → t → bool.
End Int64_signature.
Require Export TezosOfOCaml.Environment.V8.Int64.
Module Int64_check : Int64_signature := Int64.

Module Type Format_signature.
  Parameter formatter : Set.

  Parameter pp_open_box : formatter → int → unit.

  Parameter pp_close_box : formatter → unit → unit.

  Parameter pp_open_hbox : formatter → unit → unit.

  Parameter pp_open_vbox : formatter → int → unit.

  Parameter pp_open_hvbox : formatter → int → unit.

  Parameter pp_open_hovbox : formatter → int → unit.

  Parameter pp_print_string : formatter → string → unit.

  Parameter pp_print_as : formatter → int → string → unit.

  Parameter pp_print_int : formatter → int → 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 → int → int → unit.

  Parameter pp_print_custom_break :
    formatter → string × int × string → string × int × string → 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 → int → unit.

  Parameter pp_get_margin : formatter → unit → int.

  Parameter pp_set_max_indent : formatter → int → unit.

  Parameter pp_get_max_indent : formatter → unit → int.

  Parameter pp_set_max_boxes : formatter → int → unit.

  Parameter pp_get_max_boxes : formatter → unit → int.

  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 → int → int → unit.

  Parameter pp_set_ellipsis_text : formatter → string → unit.

  Parameter pp_get_ellipsis_text : formatter → unit → string.

  Parameter pp_print_list : ∀ {a : Set},
    option (formatter → unit → unit) → (formatter → a → unit) →
    formatter → list a → unit.

  Parameter pp_print_text : formatter → string → unit.

  Parameter pp_print_option : ∀ {a : Set},
    option (formatter → unit → unit) → (formatter → a → unit) →
    formatter → option a → unit.

  Parameter pp_print_result : ∀ {a e : Set},
    (formatter → a → unit) → (formatter → e → unit) → formatter →
    Pervasives.result a e → unit.

  Parameter fprintf : ∀ {a : Set},
    formatter → Pervasives.format a formatter unit → a.

  Parameter sprintf : ∀ {a : Set}, Pervasives.format a unit string → a.

  Parameter asprintf : ∀ {a : Set},
    Pervasives.format4 a formatter unit string → a.

  Parameter dprintf : ∀ {a : Set},
    Pervasives.format4 a formatter unit (formatter → unit) → a.

  Parameter ifprintf : ∀ {a : Set},
    formatter → Pervasives.format a formatter unit → a.

  Parameter kfprintf : ∀ {a b : Set},
    (formatter → a) → formatter → Pervasives.format4 b formatter unit a → b.

  Parameter kdprintf : ∀ {a b : Set},
    ((formatter → unit) → a) → Pervasives.format4 b formatter unit a → b.

  Parameter ikfprintf : ∀ {a b : Set},
    (formatter → a) → formatter → Pervasives.format4 b formatter unit a → b.

  Parameter ksprintf : ∀ {a b : Set},
    (string → a) → Pervasives.format4 b unit string a → b.

  Parameter kasprintf : ∀ {a b : Set},
    (string → a) → Pervasives.format4 b formatter unit a → b.
End Format_signature.
Require Export TezosOfOCaml.Environment.V8.Format.
Module Format_check : Format_signature := Format.

Module Type Logging_signature.
  Inductive level : Set :=
  | Debug : level
  | Info : level
  | Notice : level
  | Warning : level
  | Error : level
  | Fatal : level.

  Parameter log : ∀ {a : Set},
    level → Pervasives.format4 a Format.formatter unit unit → a.

  Parameter log_string : level → string → unit.
End Logging_signature.
Require Export TezosOfOCaml.Environment.V8.Logging.
Module Logging_check : Logging_signature := Logging.

Module Type Hex_signature.
  Inductive t : Set :=
  | Hex : string → t.

  Parameter of_char : ascii → ascii × ascii.

  Parameter to_char : ascii → ascii → option ascii.

  Parameter of_string : option (list ascii) → string → t.

  Parameter to_string : t → option string.

  Parameter of_bytes : option (list ascii) → bytes → t.

  Parameter to_bytes : t → option bytes.

  Parameter hexdump_s : option bool → option bool → t → string.

  Parameter pp : Format.formatter → t → unit.

  Parameter show : t → string.
End Hex_signature.
Require Export TezosOfOCaml.Environment.V8.Hex.
Module Hex_check : Hex_signature := Hex.

Module Type Z_signature.
  Parameter t : Set.

  Parameter zero : t.

  Parameter one : t.

  Parameter minus_one : t.

  Parameter of_int : int → t.

  Parameter of_int32 : int32 → t.

  Parameter of_int64 : int64 → t.

  Parameter of_string : string → t.

  Parameter of_substring : string → int → int → t.

  Parameter of_string_base : int → string → t.

  Parameter of_substring_base : int → string → int → int → t.

  Parameter succ : t → t.

  Parameter pred : 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 div : t → t → t.

  Parameter rem : t → t → t.

  Parameter div_rem : t → t → t × t.

  Parameter cdiv : t → t → t.

  Parameter fdiv : t → t → t.

  Parameter ediv_rem : t → t → t × t.

  Parameter ediv : t → t → t.

  Parameter erem : t → t → t.

  Parameter divexact : t → t → t.

  Parameter divisible : t → t → bool.

  Parameter congruent : t → t → t → bool.

  Parameter logand : t → t → t.

  Parameter logor : t → t → t.

  Parameter logxor : t → t → t.

  Parameter lognot : t → t.

  Parameter shift_left : t → int → t.

  Parameter shift_right : t → int → t.

  Parameter shift_right_trunc : t → int → t.

  Parameter numbits : t → int.

  Parameter trailing_zeros : t → int.

  Parameter testbit : t → int → bool.

  Parameter popcount : t → int.

  Parameter hamdist : t → t → int.

  Parameter to_int : t → int.

  Parameter to_int32 : t → int32.

  Parameter to_int64 : t → int64.

  Parameter to_string : t → string.

  Parameter format : string → t → string.

  Parameter fits_int : t → bool.

  Parameter fits_int32 : t → bool.

  Parameter fits_int64 : t → bool.

  Parameter pp_print : Format.formatter → t → unit.

  Parameter compare : t → t → int.

  Parameter equal : t → t → bool.

  Parameter leq : t → t → bool.

  Parameter geq : t → t → bool.

  Parameter lt : t → t → bool.

  Parameter gt : t → t → bool.

  Parameter sign : t → int.

  Parameter min : t → t → t.

  Parameter max : t → t → t.

  Parameter is_even : t → bool.

  Parameter is_odd : t → bool.

  Parameter pow : t → int → t.

  Parameter sqrt : t → t.

  Parameter sqrt_rem : t → t × t.

  Parameter root_value : t → int → t.

  Parameter rootrem : t → int → t × t.

  Parameter perfect_power : t → bool.

  Parameter perfect_square : t → bool.

  Parameter log2 : t → int.

  Parameter log2up : t → int.

  Parameter size_value : t → int.

  Parameter extract : t → int → int → t.

  Parameter signed_extract : t → int → int → t.

  Parameter to_bits : t → string.

  Parameter of_bits : string → t.
End Z_signature.
Require Export TezosOfOCaml.Environment.V8.Z.
Module Z_check : Z_signature := Z.

Module Type Q_signature.
  Module t.
    Record record : Set := Build {
      num : Z.t;
      den : Z.t;
    }.
    Definition with_num num (r : record) :=
      Build num r.(den).
    Definition with_den den (r : record) :=
      Build r.(num) den.
  End t.
  Definition t := t.record.

  Parameter make : Z.t → Z.t → t.

  Parameter zero : t.

  Parameter one : t.

  Parameter minus_one : t.

  Parameter inf : t.

  Parameter minus_inf : t.

  Parameter undef : t.

  Parameter of_bigint : Z.t → t.

  Parameter of_int : int → t.

  Parameter of_int32 : int32 → t.

  Parameter of_int64 : int64 → t.

  Parameter of_ints : int → int → t.

  Parameter of_string : string → t.

  Parameter num : t → Z.t.

  Parameter den : t → Z.t.

  Inductive kind : Set :=
  | ZERO : kind
  | INF : kind
  | MINF : kind
  | UNDEF : kind
  | NZERO : kind.

  Parameter classify : t → kind.

  Parameter is_real : t → bool.

  Parameter sign : t → int.

  Parameter compare : t → t → int.

  Parameter equal : t → t → bool.

  Parameter min : t → t → t.

  Parameter max : t → t → t.

  Parameter leq : t → t → bool.

  Parameter geq : t → t → bool.

  Parameter lt : t → t → bool.

  Parameter gt : t → t → bool.

  Parameter to_bigint : t → Z.t.

  Parameter to_int : t → int.

  Parameter to_int32 : t → int32.

  Parameter to_int64 : t → int64.

  Parameter to_string : t → string.

  Parameter neg : t → t.

  Parameter abs : t → t.

  Parameter add : t → t → t.

  Parameter sub : t → t → t.

  Parameter mul : t → t → t.

  Parameter inv : t → t.

  Parameter div : t → t → t.

  Parameter mul_2exp : t → int → t.

  Parameter div_2exp : t → int → t.

  Parameter pp_print : Format.formatter → t → unit.

  Parameter op_tildeminus : t → t.

  Parameter op_tildeplus : t → t.

  Parameter op_plus : t → t → t.

  Parameter op_minus : t → t → t.

  Parameter op_star : t → t → t.

  Parameter op_div : t → t → t.

  Parameter lsl : t → int → t.

  Parameter asr : t → int → t.

  Parameter op_tildedollar : int → t.

  Parameter op_divdiv : int → int → t.

  Parameter op_tildedollardollar : Z.t → t.

  Parameter op_divdivdiv : Z.t → Z.t → t.

  Parameter op_eq : t → t → bool.

  Parameter op_lt : t → t → bool.

  Parameter op_gt : t → t → bool.

  Parameter op_lteq : t → t → bool.

  Parameter op_gteq : t → t → bool.

  Parameter op_ltgt : t → t → bool.
End Q_signature.
Require Export TezosOfOCaml.Environment.V8.Q.
Module Q_check : Q_signature := Q.

Module Type Lwt_signature.
  Parameter t : ∀ (a : Set), Set.

  Parameter _return : ∀ {a : Set}, a → t a.

  Parameter bind : ∀ {a b : Set}, t a → (a → t b) → t b.

  Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.

  Parameter return_unit : t unit.

  Parameter return_none : ∀ {A : Set}, t (option A).

  Parameter return_nil : ∀ {A : Set}, t (list A).

  Parameter return_true : t bool.

  Parameter return_false : t bool.

  Parameter return_some : ∀ {a : Set}, a → t (option a).

  Parameter return_ok : ∀ {B a : Set}, a → t (Pervasives.result a B).

  Parameter return_error : ∀ {B e : Set}, e → t (Pervasives.result B e).
End Lwt_signature.
(* We do not implement the Lwt module, as it is the identity monad for us since
   the protocol code is sequential and interactions with the store can be
   implemented in a purely functional way. *)

Module Type Data_encoding_signature.
  Inductive json : Set :=
  | Bool : bool → json
  | Null : json
  | O : list (string × json) → json
  | Float : float → json
  | String : string → json
  | A : list json → json.

  Inductive tag_size : Set :=
  | Uint16 : tag_size
  | Uint8 : tag_size.

  Parameter json_schema : Set.

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

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

  Inductive string_json_repr : Set :=
  | Hex : string_json_repr
  | Plain : string_json_repr.

  Parameter classify : ∀ {a : Set}, encoding a → Variant.t.

  Parameter null : encoding unit.

  Parameter empty : encoding unit.

  Parameter unit_value : encoding unit.

  Parameter constant : string → encoding unit.

  Parameter int8 : encoding int.

  Parameter uint8 : encoding int.

  Parameter int16 : encoding int.

  Parameter uint16 : encoding int.

  Parameter int31 : encoding int.

  Parameter int32_value : encoding int32.

  Parameter int64_value : encoding int64.

  Parameter ranged_int : int → int → encoding int.

  Parameter z_value : encoding Z.t.

  Parameter n_value : encoding Z.t.

  Parameter uint_like_n : option int → unit → encoding int.

  Parameter int_like_z : option int → option int → unit → encoding int.

  Parameter bool_value : encoding bool.

  Parameter string' : option Variant.t → string_json_repr → encoding string.

  Parameter bytes' : option Variant.t → string_json_repr → encoding Bytes.t.

  Parameter string_value : encoding string.

  Parameter bytes_value : encoding Bytes.t.

  Parameter option_value : ∀ {a : Set}, encoding a → encoding (option a).

  Parameter result_value : ∀ {a b : Set},
    encoding a → encoding b → encoding (Pervasives.result a b).

  Parameter list_value : ∀ {a : Set},
    option int → encoding a → encoding (list a).

  Parameter list_with_length : ∀ {a : Set},
    option int → Variant.t → encoding a → encoding (list a).

  Parameter conv : ∀ {a b : Set},
    (a → b) → (b → a) → option json_schema → encoding b → encoding a.

  Parameter conv_with_guard : ∀ {a b : Set},
    (a → b) → (b → Pervasives.result a string) → option json_schema →
    encoding b → encoding a.

  Parameter with_decoding_guard : ∀ {a : Set},
    (a → Pervasives.result unit string) → encoding a → encoding a.

  Parameter assoc : ∀ {a : Set},
    encoding a → encoding (list (string × a)).

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

  Parameter req : ∀ {t : Set},
    option string → option string → string → encoding t → field t.

  Parameter opt : ∀ {t : Set},
    option string → option string → string → encoding t → field (option t).

  Parameter varopt : ∀ {t : Set},
    option string → option string → string → encoding t → field (option t).

  Parameter dft : ∀ {t : Set},
    option string → option string → string → encoding t → t → field t.

  Parameter obj1 : ∀ {f1 : Set}, field f1 → encoding f1.

  Parameter obj2 : ∀ {f1 f2 : Set},
    field f1 → field f2 → encoding (f1 × f2).

  Parameter obj3 : ∀ {f1 f2 f3 : Set},
    field f1 → field f2 → field f3 → encoding (f1 × f2 × f3).

  Parameter obj4 : ∀ {f1 f2 f3 f4 : Set},
    field f1 → field f2 → field f3 → field f4 → encoding (f1 × f2 × f3 × f4).

  Parameter obj5 : ∀ {f1 f2 f3 f4 f5 : Set},
    field f1 → field f2 → field f3 → field f4 → field f5 →
    encoding (f1 × f2 × f3 × f4 × f5).

  Parameter obj6 : ∀ {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 : ∀ {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 : ∀ {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 : ∀ {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 : ∀ {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 merge_objs : ∀ {o1 o2 : Set},
    encoding o1 → encoding o2 → encoding (o1 × o2).

  Module With_field_name_duplicate_checks.
    Parameter obj1 : ∀ {f1 : Set}, field f1 → encoding f1.

    Parameter obj2 : ∀ {f1 f2 : Set},
      field f1 → field f2 → encoding (f1 × f2).

    Parameter obj3 : ∀ {f1 f2 f3 : Set},
      field f1 → field f2 → field f3 → encoding (f1 × f2 × f3).

    Parameter obj4 : ∀ {f1 f2 f3 f4 : Set},
      field f1 → field f2 → field f3 → field f4 →
      encoding (f1 × f2 × f3 × f4).

    Parameter obj5 : ∀ {f1 f2 f3 f4 f5 : Set},
      field f1 → field f2 → field f3 → field f4 → field f5 →
      encoding (f1 × f2 × f3 × f4 × f5).

    Parameter obj6 : ∀ {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 : ∀ {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 : ∀ {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 : ∀ {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 : ∀ {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 merge_objs : ∀ {o1 o2 : Set},
      encoding o1 → encoding o2 → encoding (o1 × o2).
  End With_field_name_duplicate_checks.

  Parameter tup1 : ∀ {f1 : Set}, encoding f1 → encoding f1.

  Parameter tup2 : ∀ {f1 f2 : Set},
    encoding f1 → encoding f2 → encoding (f1 × f2).

  Parameter tup3 : ∀ {f1 f2 f3 : Set},
    encoding f1 → encoding f2 → encoding f3 → encoding (f1 × f2 × f3).

  Parameter tup4 : ∀ {f1 f2 f3 f4 : Set},
    encoding f1 → encoding f2 → encoding f3 → encoding f4 →
    encoding (f1 × f2 × f3 × f4).

  Parameter tup5 : ∀ {f1 f2 f3 f4 f5 : Set},
    encoding f1 → encoding f2 → encoding f3 → encoding f4 → encoding f5 →
    encoding (f1 × f2 × f3 × f4 × f5).

  Parameter tup6 : ∀ {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 : ∀ {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 : ∀ {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 : ∀ {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 : ∀ {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_tups : ∀ {a1 a2 : Set},
    encoding a1 → encoding a2 → encoding (a1 × a2).

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

  Inductive case_tag : Set :=
  | Tag : int → case_tag
  | Json_only : case_tag.

  Parameter match_result : Set.

  Definition matching_function (a : Set) : Set := a → match_result.

  Parameter matched : ∀ {a : Set},
    option Variant.t → int → encoding a → a → match_result.

  Parameter case_value : ∀ {a t : Set},
    string → option string → case_tag → encoding a → (t → option a) →
    (a → t) → case t.

  Parameter matching : ∀ {t : Set},
    option Variant.t → matching_function t → list (case t) → encoding t.

  Parameter union : ∀ {t : Set},
    option Variant.t → list (case t) → encoding t.

  Module With_JSON_discriminant.
    Inductive case_tag : Set :=
    | Tag : int × string → case_tag.

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

    Parameter case_value : ∀ {a t : Set},
      string → option string → case_tag → encoding a → (t → option a) →
      (a → t) → case t.

    Parameter matched : ∀ {a : Set},
      option Variant.t → int × string → encoding a → a → match_result.

    Parameter matching : ∀ {t : Set},
      option Variant.t → matching_function t → list (case t) → encoding t.

    Parameter union : ∀ {t : Set},
      option Variant.t → list (case t) → encoding t.
  End With_JSON_discriminant.

  Parameter string_enum : ∀ {a : Set}, list (string × a) → encoding a.

  Module Fixed.
    Parameter string_value : int → encoding string.

    Parameter string' : string_json_repr → int → encoding string.

    Parameter bytes_value : int → encoding Bytes.t.

    Parameter bytes' : string_json_repr → int → encoding Bytes.t.

    Parameter add_padding : ∀ {a : Set}, encoding a → int → encoding a.

    Parameter list_value : ∀ {a : Set},
      int → encoding a → encoding (list a).

    Parameter array_value : ∀ {a : Set},
      int → encoding a → encoding (array a).
  End Fixed.

  Module _Variable.
    Parameter string_value : encoding string.

    Parameter string' : string_json_repr → encoding string.

    Parameter bytes_value : encoding Bytes.t.

    Parameter bytes' : string_json_repr → encoding Bytes.t.

    Parameter array_value : ∀ {a : Set},
      option int → encoding a → encoding (array a).

    Parameter list_value : ∀ {a : Set},
      option int → encoding a → encoding (list a).
  End _Variable.

  Module Bounded.
    Parameter string' :
      option Variant.t → string_json_repr → int → encoding string.

    Parameter string_value : int → encoding string.

    Parameter bytes' :
      option Variant.t → string_json_repr → int → encoding Bytes.t.

    Parameter bytes_value : int → encoding Bytes.t.
  End Bounded.

  Parameter dynamic_size : ∀ {a : Set},
    option Variant.t → encoding a → encoding a.

  Parameter check_size : ∀ {a : Set}, int → encoding a → encoding a.

  Parameter splitted : ∀ {a : Set}, encoding a → encoding a → encoding a.

  Parameter mu : ∀ {a : Set},
    string → option string → option string → (encoding a → encoding a) →
    encoding a.

  Parameter def : ∀ {t : Set},
    string → option string → option string → encoding t → encoding t.

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

  Parameter lazy_encoding : ∀ {a : Set}, encoding a → encoding (lazy_t a).

  Parameter force_decode : ∀ {a : Set}, lazy_t a → option a.

  Parameter force_bytes : ∀ {a : Set}, lazy_t a → bytes.

  Parameter make_lazy : ∀ {a : Set}, encoding a → a → lazy_t a.

  Parameter apply_lazy : ∀ {a b : Set},
    (a → b) → (bytes → b) → (b → b → b) → lazy_t a → b.

  Module Compact.
    Parameter t : ∀ (a : Set), Set.

    Parameter make : ∀ {a : Set}, option Variant.t → t a → encoding a.

    Parameter tag_bit_count : ∀ {a : Set}, t a → int.

    Parameter void : Set.

    Parameter void_value : t void.

    Parameter refute : ∀ {a : Set}, void → a.

    Parameter unit_value : t unit.

    Parameter null : t unit.

    Parameter bool_value : t bool.

    Parameter payload : ∀ {a : Set}, encoding a → t a.

    Parameter option_value : ∀ {a : Set}, t a → t (option a).

    Parameter conv : ∀ {a b : Set},
      option (encoding a) → (a → b) → (b → a) → t b → t a.

    Parameter tup1 : ∀ {a : Set}, t a → t a.

    Parameter tup2 : ∀ {a b : Set}, t a → t b → t (a × b).

    Parameter tup3 : ∀ {a b c : Set}, t a → t b → t c → t (a × b × c).

    Parameter tup4 : ∀ {a b c d : Set},
      t a → t b → t c → t d → t (a × b × c × d).

    Parameter tup5 : ∀ {f1 f2 f3 f4 f5 : Set},
      t f1 → t f2 → t f3 → t f4 → t f5 → t (f1 × f2 × f3 × f4 × f5).

    Parameter tup6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
      t f1 → t f2 → t f3 → t f4 → t f5 → t f6 →
      t (f1 × f2 × f3 × f4 × f5 × f6).

    Parameter tup7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
      t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 →
      t (f1 × f2 × f3 × f4 × f5 × f6 × f7).

    Parameter tup8 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 : Set},
      t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 →
      t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).

    Parameter tup9 : ∀ {f1 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
      t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 → t f9 →
      t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).

    Parameter tup10 : ∀ {f1 f10 f2 f3 f4 f5 f6 f7 f8 f9 : Set},
      t f1 → t f2 → t f3 → t f4 → t f5 → t f6 → t f7 → t f8 → t f9 →
      t f10 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).

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

    Parameter req : ∀ {a : Set}, string → t a → field a.

    Parameter opt : ∀ {a : Set}, string → t a → field (option a).

    Parameter obj1 : ∀ {a : Set}, field a → t a.

    Parameter obj2 : ∀ {a b : Set}, field a → field b → t (a × b).

    Parameter obj3 : ∀ {a b c : Set},
      field a → field b → field c → t (a × b × c).

    Parameter obj4 : ∀ {a b c d : Set},
      field a → field b → field c → field d → t (a × b × c × d).

    Parameter obj5 : ∀ {f1 f2 f3 f4 f5 : Set},
      field f1 → field f2 → field f3 → field f4 → field f5 →
      t (f1 × f2 × f3 × f4 × f5).

    Parameter obj6 : ∀ {f1 f2 f3 f4 f5 f6 : Set},
      field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
      t (f1 × f2 × f3 × f4 × f5 × f6).

    Parameter obj7 : ∀ {f1 f2 f3 f4 f5 f6 f7 : Set},
      field f1 → field f2 → field f3 → field f4 → field f5 → field f6 →
      field f7 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7).

    Parameter obj8 : ∀ {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 → t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8).

    Parameter obj9 : ∀ {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 →
      t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9).

    Parameter obj10 : ∀ {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 →
      t (f1 × f2 × f3 × f4 × f5 × f6 × f7 × f8 × f9 × f10).

    Parameter int32_value : t int32.

    Parameter int64_value : t int64.

    Parameter list_value : ∀ {a : Set}, int → encoding a → t (list a).

    Parameter case : ∀ (a : Set), Set.

    Parameter case_value : ∀ {a b : Set},
      string → option string → t b → (a → option b) → (b → a) → case a.

    Parameter union : ∀ {a : Set},
      option int → option int → list (case a) → t a.

    Parameter void_case : ∀ {a : Set}, string → case a.

    Parameter or_int32 : ∀ {a : Set},
      string → string → option string → encoding a → t (Either.t int32 a).

    Module Custom.
      Definition tag : Set := int.

      Parameter join_tags : list (tag × int) → tag.

      Module S.
        Record signature {input layout : Set} : Set := {
          

The type of [input] this module allows to encode.

          input := input;
          

The various ways to efficiently encode [input].

          layout := layout;
          

The list of layouts available to encode [input].

          layouts : list layout;
          

The number of bits necessary to distinguish between the various layouts.

          tag_len : int;
          

[tag layout] computes the tag of {!Data_encoding.union} to be used to encode values classified as [layout].

{b Warning:} It is expected that [tag layout < 2^tag_len - 1].

          tag : layout → tag;
          

[partial_encoding layout] returns the encoding to use for values classified as [layout].

This encoding can be partial in the sense that it may fail (it will raise an [Invalid_argument]) for some values of [x]. However, it is expected that [partial_encoding (classify x) x] will always succeed.

          partial_encoding : layout → encoding input;
          

[classify x] returns the layout to be used to encode [x].

          classify : input → layout;
          

The encoding to use when targeting a JSON output.

          json_encoding : encoding input;
        }.
      End S.
      Definition S := @S.signature.
      Arguments S {_ _}.

      Parameter make : ∀ {a : Set},
        {layout : Set @ S (input := a) (layout := layout)} → t a.
    End Custom.
  End Compact.

  Definition compact (a : Set) : Set := Compact.t a.

  Parameter json_value : encoding json.

  Parameter json_schema_value : encoding json_schema.

  Module Json.
    Parameter schema : ∀ {a : Set},
      option string → encoding a → json_schema.

    Parameter construct : ∀ {t : Set},
      option Variant.t → encoding t → t → json.

    Parameter destruct : ∀ {t : Set},
      option bool → encoding t → json → t.

    Reserved Notation "'path".

    Inductive path_item : Set :=
    | Index : int → path_item
    | Field : string → path_item
    | Next : path_item
    | Star : path_item
    
    where "'path" := (list path_item).

    Definition path := 'path.

    Parameter print_error :
      option (Format.formatter → extensible_type → unit) →
      Format.formatter → extensible_type → unit.

    Parameter cannot_destruct : ∀ {a b : Set},
      Pervasives.format4 a Format.formatter unit b → a.

    Parameter wrap_error : ∀ {a b : Set}, (a → b) → a → b.

    Parameter pp : Format.formatter → json → unit.
  End Json.

  Module Binary.
    Parameter length : ∀ {a : Set}, encoding a → a → int.

    Parameter fixed_length : ∀ {a : Set}, encoding a → option int.

    Parameter maximum_length : ∀ {a : Set}, encoding a → option int.

    Parameter of_bytes_opt : ∀ {a : Set}, encoding a → bytes → option a.

    Parameter of_string_opt : ∀ {a : Set},
      encoding a → string → option a.

    Parameter to_bytes_opt : ∀ {a : Set},
      option int → encoding a → a → option bytes.

    Parameter to_bytes_exn : ∀ {a : Set},
      option int → encoding a → a → bytes.

    Parameter to_string_opt : ∀ {a : Set},
      option int → encoding a → a → option string.

    Parameter to_string_exn : ∀ {a : Set},
      option int → encoding a → a → string.
  End Binary.
End Data_encoding_signature.
Require Export TezosOfOCaml.Environment.V8.Data_encoding.
Module Data_encoding_check : Data_encoding_signature := Data_encoding.

Module Type Raw_hashes_signature.
  Parameter blake2b : bytes → bytes.

  Parameter sha256 : bytes → bytes.

  Parameter sha512 : bytes → bytes.

  Parameter keccak256 : bytes → bytes.

  Parameter sha3_256 : bytes → bytes.

  Parameter sha3_512 : bytes → bytes.
End Raw_hashes_signature.
Require Export TezosOfOCaml.Environment.V8.Raw_hashes.
Module Raw_hashes_check : Raw_hashes_signature := Raw_hashes.

Module Type Compare_signature.
  Module COMPARABLE.
    Record signature {t : Set} : Set := {
      t := t;
      compare : t → t → int;
    }.
  End COMPARABLE.
  Definition COMPARABLE := @COMPARABLE.signature.
  Arguments COMPARABLE {_}.

  Module S.
    Record signature {t : Set} : Set := {
      t := t;
      

[x = y] iff [compare x y = 0]

      op_eq : t → t → bool;
      

[x <> y] iff [compare x y <> 0]

      op_ltgt : t → t → bool;
      

[x < y] iff [compare x y < 0]

      op_lt : t → t → bool;
      

[x <= y] iff [compare x y <= 0]

      op_lteq : t → t → bool;
      

[x >= y] iff [compare x y >= 0]

      op_gteq : t → t → bool;
      

[x > y] iff [compare x y > 0]

      op_gt : t → t → bool;
      

[compare] an alias for the functor parameter's [compare] function

      compare : t → t → int;
      

[equal x y] iff [compare x y = 0]

      equal : t → t → bool;
      

[max x y] is [x] if [x >= y] otherwise it is [y]

      max : t → t → t;
      

[min x y] is [x] if [x <= y] otherwise it is [y]

      min : t → t → t;
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_}.

  Parameter Make :
    ∀ {P_t : Set},
    ∀ (P : COMPARABLE (t := P_t)), S (t := P.(COMPARABLE.t)).

  Parameter Char : S (t := ascii).

  Parameter Bool : S (t := bool).

  Module Int.
    Definition t : Set := int.

    Parameter op_eq : int → int → bool.

    Parameter op_ltgt : int → int → bool.

    Parameter op_lt : int → int → bool.

    Parameter op_gt : int → int → bool.

    Parameter op_lteq : int → int → bool.

    Parameter op_gteq : int → int → bool.

    Parameter compare : int → int → int.

    Parameter max : int → int → int.

    Parameter min : int → int → int.

    Parameter equal : int → int → bool.
  End Int.

  Parameter Int32 : S (t := int32).

  Parameter Uint32 : S (t := int32).

  Parameter Int64 : S (t := int64).

  Parameter Uint64 : S (t := int64).

  Parameter String : S (t := string).

  Parameter Bytes : S (t := bytes).

  Parameter Z : S (t := Z.t).

  Parameter Q : S (t := Q.t).

  Parameter List :
    ∀ {P_t : Set},
    ∀ (P : COMPARABLE (t := P_t)), S (t := list P.(COMPARABLE.t)).

  Parameter Option :
    ∀ {P_t : Set},
    ∀ (P : COMPARABLE (t := P_t)), S (t := option P.(COMPARABLE.t)).

  Parameter Result :
    ∀ {Ok_t Error_t : Set},
    ∀ (Ok : COMPARABLE (t := Ok_t)),
    ∀ (Error : COMPARABLE (t := Error_t)),
    S (t := Pervasives.result Ok.(COMPARABLE.t) Error.(COMPARABLE.t)).

  Module List_length_with.
    Parameter op_eq : ∀ {a : Set}, list a → int → bool.

    Parameter op_ltgt : ∀ {a : Set}, list a → int → bool.

    Parameter op_lt : ∀ {a : Set}, list a → int → bool.

    Parameter op_lteq : ∀ {a : Set}, list a → int → bool.

    Parameter op_gteq : ∀ {a : Set}, list a → int → bool.

    Parameter op_gt : ∀ {a : Set}, list a → int → bool.

    Parameter compare : ∀ {a : Set}, list a → int → int.

    Parameter equal : ∀ {a : Set}, list a → int → bool.
  End List_length_with.

  Module List_lengths.
    Parameter op_eq : ∀ {a b : Set}, list a → list b → bool.

    Parameter op_ltgt : ∀ {a b : Set}, list a → list b → bool.

    Parameter op_lt : ∀ {a b : Set}, list a → list b → bool.

    Parameter op_lteq : ∀ {a b : Set}, list a → list b → bool.

    Parameter op_gteq : ∀ {a b : Set}, list a → list b → bool.

    Parameter op_gt : ∀ {a b : Set}, list a → list b → bool.

    Parameter compare : ∀ {a b : Set}, list a → list b → int.

    Parameter equal : ∀ {a b : Set}, list a → list b → bool.
  End List_lengths.

  Parameter or_else : int → (unit → int) → int.
End Compare_signature.
Require Export TezosOfOCaml.Environment.V8.Compare.
Module Compare_check : Compare_signature := Compare.

Module Type Time_signature.
  Parameter t : Set.

  Parameter Included_S : Compare.S (t := t).

  Definition op_eq : t → t → bool := Included_S.(Compare.S.op_eq).

  Definition op_ltgt : t → t → bool := Included_S.(Compare.S.op_ltgt).

  Definition op_lt : t → t → bool := Included_S.(Compare.S.op_lt).

  Definition op_lteq : t → t → bool := Included_S.(Compare.S.op_lteq).

  Definition op_gteq : t → t → bool := Included_S.(Compare.S.op_gteq).

  Definition op_gt : t → t → bool := Included_S.(Compare.S.op_gt).

  Definition compare : t → t → int := Included_S.(Compare.S.compare).

  Definition equal : t → t → bool := Included_S.(Compare.S.equal).

  Definition max : t → t → t := Included_S.(Compare.S.max).

  Definition min : t → t → t := Included_S.(Compare.S.min).

  Parameter add : t → int64 → t.

  Parameter diff_value : 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_signature.
Require Export TezosOfOCaml.Environment.V8.Time.
Module Time_check : Time_signature := Time.

Module Type TzEndian_signature.
  Parameter get_int32 : bytes → int → int32.

  Parameter get_int32_string : string → int → int32.

  Parameter set_int32 : bytes → int → int32 → unit.

  Parameter set_int8 : bytes → int → int → unit.

  Parameter get_int8 : bytes → int → int.

  Parameter get_int8_string : string → int → int.

  Parameter set_int16 : bytes → int → int → unit.

  Parameter get_int16 : bytes → int → int.

  Parameter get_int16_string : string → int → int.

  Parameter set_int64 : bytes → int → int64 → unit.

  Parameter get_int64 : bytes → int → int64.

  Parameter get_int64_string : string → int → int64.

  Parameter get_uint8 : bytes → int → int.

  Parameter get_uint8_string : string → int → int.

  Parameter set_uint8 : bytes → int → int → unit.

  Parameter get_uint16 : bytes → int → int.

  Parameter get_uint16_string : string → int → int.

  Parameter set_uint16 : bytes → int → int → unit.
End TzEndian_signature.
Require Export TezosOfOCaml.Environment.V8.TzEndian.
Module TzEndian_check : TzEndian_signature := TzEndian.

Module Type Bits_signature.
  Parameter numbits : int → int.
End Bits_signature.
Require Export TezosOfOCaml.Environment.V8.Bits.
Module Bits_check : Bits_signature := Bits.

Module Type Equality_witness_signature.
  Inductive eq : Set :=
  | Refl : eq.

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

  Parameter make : ∀ {a : Set}, unit → t a.

  Parameter eq_value : ∀ {a b : Set}, t a → t b → option eq.

  Parameter hash_value : ∀ {a : Set}, t a → int.
End Equality_witness_signature.
Require Export TezosOfOCaml.Environment.V8.Equality_witness.
Module Equality_witness_check : Equality_witness_signature := Equality_witness.

Module Type FallbackArray_signature.
  Parameter t : ∀ (a : Set), Set.

  Parameter make : ∀ {a : Set}, int → a → t a.

  Parameter of_list : ∀ {a b : Set}, b → (a → b) → list a → t b.

  Parameter fallback : ∀ {a : Set}, t a → a.

  Parameter length : ∀ {a : Set}, t a → int.

  Parameter get : ∀ {a : Set}, t a → int → a.

  Parameter set : ∀ {a : Set}, t a → int → a → unit.

  Parameter iter : ∀ {a : Set}, (a → unit) → t a → unit.

  Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.

  Parameter fold : ∀ {a b : Set}, (b → a → b) → t a → b → b.

  Parameter fold_map : ∀ {a b c : Set},
    (b → a → b × c) → t a → b → c → b × t c.
End FallbackArray_signature.
Require Export TezosOfOCaml.Environment.V8.FallbackArray.
Module FallbackArray_check : FallbackArray_signature := FallbackArray.

Module Type Error_monad_signature.
  Inductive error_category : Set :=
  | Outdated : error_category
  | Permanent : error_category
  | Temporary : error_category
  | Branch : error_category.

  Definition _error := extensible_type.

  Parameter error_encoding : Data_encoding.t _error.

  Parameter pp : Format.formatter → _error → unit.

  Parameter register_error_kind : ∀ {err : Set},
    error_category → string → string → string →
    option (Format.formatter → err → unit) → Data_encoding.t err →
    (_error → option err) → (err → _error) → unit.

  Parameter json_of_error : _error → Data_encoding.json.

  Parameter error_of_json : Data_encoding.json → _error.

  Module error_info.
    Record record : Set := Build {
      category : error_category;
      id : string;
      title : string;
      description : string;
      schema : Data_encoding.json_schema;
    }.
    Definition with_category category (r : record) :=
      Build category r.(id) r.(title) r.(description) r.(schema).
    Definition with_id id (r : record) :=
      Build r.(category) id r.(title) r.(description) r.(schema).
    Definition with_title title (r : record) :=
      Build r.(category) r.(id) title r.(description) r.(schema).
    Definition with_description description (r : record) :=
      Build r.(category) r.(id) r.(title) description r.(schema).
    Definition with_schema schema (r : record) :=
      Build r.(category) r.(id) r.(title) r.(description) 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 trace : ∀ (err : Set), Set.

  Definition tzresult (a : Set) : Set := Pervasives.result a (trace _error).

  Parameter make_trace_encoding : ∀ {_error : Set},
    Data_encoding.t _error → Data_encoding.t (trace _error).

  Parameter trace_encoding : Data_encoding.t (trace _error).

  Parameter pp_trace : Format.formatter → trace _error → unit.

  Parameter result_encoding : ∀ {a : Set},
    Data_encoding.t a → Data_encoding.t (tzresult a).

  Parameter ok : ∀ {a trace : Set}, a → Pervasives.result a trace.

  Parameter _return : ∀ {a trace : Set}, a → Pervasives.result a trace.

  Parameter return_unit : ∀ {trace : Set}, Pervasives.result unit trace.

  Parameter return_none : ∀ {a trace : Set},
    Pervasives.result (option a) trace.

  Parameter return_some : ∀ {a trace : Set},
    a → Pervasives.result (option a) trace.

  Parameter return_nil : ∀ {a trace : Set},
    Pervasives.result (list a) trace.

  Parameter return_true : ∀ {trace : Set}, Pervasives.result bool trace.

  Parameter return_false : ∀ {trace : Set}, Pervasives.result bool trace.

  Parameter error_value : ∀ {a err : Set},
    err → Pervasives.result a (trace err).

  Parameter trace_of_error : ∀ {err : Set}, err → trace err.

  Parameter tzfail : ∀ {a err : Set},
    err → Pervasives.result a (trace err).

  Parameter op_gtgteq : ∀ {a b : Set}, a → (a → b) → b.

  Parameter op_gtpipeeq : ∀ {a b : Set}, a → (a → b) → b.

  Parameter op_gtgtquestion : ∀ {a b trace : Set},
    Pervasives.result a trace → (a → Pervasives.result b trace) →
    Pervasives.result b trace.

  Parameter op_gtpipequestion : ∀ {a b trace : Set},
    Pervasives.result a trace → (a → b) → Pervasives.result b trace.

  Parameter op_gtgteqquestion : ∀ {a b trace : Set},
    Pervasives.result a trace → (a → Pervasives.result b trace) →
    Pervasives.result b trace.

  Parameter op_gtpipeeqquestion : ∀ {a b trace : Set},
    Pervasives.result a trace → (a → b) → Pervasives.result b trace.

  Parameter op_gtgtquestioneq : ∀ {a b trace : Set},
    Pervasives.result a trace → (a → Pervasives.result b trace) →
    Pervasives.result b trace.

  Parameter op_gtpipequestioneq : ∀ {a b trace : Set},
    Pervasives.result a trace → (a → b) → Pervasives.result b trace.

  Parameter record_trace : ∀ {a err : Set},
    err → Pervasives.result a (trace err) → Pervasives.result a (trace err).

  Parameter trace_value : ∀ {b err : Set},
    err → Pervasives.result b (trace err) → Pervasives.result b (trace err).

  Parameter record_trace_eval : ∀ {a err : Set},
    (unit → err) → Pervasives.result a (trace err) →
    Pervasives.result a (trace err).

  Parameter trace_eval : ∀ {b err : Set},
    (unit → err) → Pervasives.result b (trace err) →
    Pervasives.result b (trace err).

  Parameter error_unless : ∀ {err : Set},
    bool → err → Pervasives.result unit (trace err).

  Parameter error_when : ∀ {err : Set},
    bool → err → Pervasives.result unit (trace err).

  Parameter fail_unless : ∀ {err : Set},
    bool → err → Pervasives.result unit (trace err).

  Parameter fail_when : ∀ {err : Set},
    bool → err → Pervasives.result unit (trace err).

  Parameter unless : ∀ {trace : Set},
    bool → (unit → Pervasives.result unit trace) →
    Pervasives.result unit trace.

  Parameter when_ : ∀ {trace : Set},
    bool → (unit → Pervasives.result unit trace) →
    Pervasives.result unit trace.

  Parameter dont_wait : ∀ {trace : Set},
    (extensible_type → unit) → (trace → unit) →
    (unit → Pervasives.result unit trace) → unit.

  Parameter catch : ∀ {a : Set},
    option (extensible_type → bool) → (unit → a) → tzresult a.

  Parameter catch_f : ∀ {a : Set},
    option (extensible_type → bool) → (unit → a) →
    (extensible_type → _error) → tzresult a.

  Parameter catch_s : ∀ {a : Set},
    option (extensible_type → bool) → (unit → a) → tzresult a.

  Parameter join_e : ∀ {err : Set},
    list (Pervasives.result unit (trace err)) →
    Pervasives.result unit (trace err).

  Parameter all_e : ∀ {a err : Set},
    list (Pervasives.result a (trace err)) →
    Pervasives.result (list a) (trace err).

  Parameter both_e : ∀ {a b err : Set},
    Pervasives.result a (trace err) → Pervasives.result b (trace err) →
    Pervasives.result (a × b) (trace err).

  Parameter shell_tztrace : Set.

  Definition shell_tzresult (a : Set) : Set :=
    Pervasives.result a shell_tztrace.

  Module Lwt_syntax.
    Parameter _return : ∀ {a : Set}, a → a.

    Parameter return_none : ∀ {A : Set}, option A.

    Parameter return_nil : ∀ {A : Set}, list A.

    Parameter return_true : bool.

    Parameter return_false : bool.

    Parameter return_some : ∀ {a : Set}, a → option a.

    Parameter return_ok : ∀ {B a : Set}, a → Pervasives.result a B.

    Parameter return_error : ∀ {B e : Set}, e → Pervasives.result B e.

    Parameter return_ok_unit : ∀ {e : Set}, Pervasives.result unit e.

    Parameter return_ok_true : ∀ {e : Set}, Pervasives.result bool e.

    Parameter return_ok_false : ∀ {e : Set}, Pervasives.result bool e.

    Parameter return_ok_none : ∀ {a e : Set},
      Pervasives.result (option a) e.

    Parameter return_ok_nil : ∀ {a e : Set}, Pervasives.result (list a) e.

    Parameter op_letstar : ∀ {a b : Set}, a → (a → b) → b.

    Parameter op_andstar : ∀ {a b : Set}, a → b → a × b.

    Parameter op_letplus : ∀ {a b : Set}, a → (a → b) → b.

    Parameter op_andplus : ∀ {a b : Set}, a → b → a × b.

    Parameter join : list unit → unit.

    Parameter all : ∀ {a : Set}, list a → list a.

    Parameter both : ∀ {a b : Set}, a → b → a × b.
  End Lwt_syntax.

  Module Option_syntax.
    Parameter _return : ∀ {a : Set}, a → option a.

    Parameter fail : ∀ {a : Set}, option a.

    Parameter return_unit : option unit.

    Parameter return_nil : ∀ {a : Set}, option (list a).

    Parameter return_true : option bool.

    Parameter return_false : option bool.

    Parameter op_letstar : ∀ {a b : Set},
      option a → (a → option b) → option b.

    Parameter op_andstar : ∀ {a b : Set},
      option a → option b → option (a × b).

    Parameter op_letplus : ∀ {a b : Set}, option a → (a → b) → option b.

    Parameter op_andplus : ∀ {a b : Set},
      option a → option b → option (a × b).

    Parameter both : ∀ {a b : Set}, option a → option b → option (a × b).
  End Option_syntax.

  Module Result_syntax.
    Parameter _return : ∀ {a e : Set}, a → Pervasives.result a e.

    Parameter return_unit : ∀ {e : Set}, Pervasives.result unit e.

    Parameter return_none : ∀ {a e : Set}, Pervasives.result (option a) e.

    Parameter return_some : ∀ {a e : Set},
      a → Pervasives.result (option a) e.

    Parameter return_nil : ∀ {a e : Set}, Pervasives.result (list a) e.

    Parameter return_true : ∀ {e : Set}, Pervasives.result bool e.

    Parameter return_false : ∀ {e : Set}, Pervasives.result bool e.

    Parameter fail : ∀ {a e : Set}, e → Pervasives.result a e.

    Parameter op_letstar : ∀ {a b e : Set},
      Pervasives.result a e → (a → Pervasives.result b e) →
      Pervasives.result b e.

    Parameter op_letplus : ∀ {a b e : Set},
      Pervasives.result a e → (a → b) → Pervasives.result b e.

    Parameter join : ∀ {e : Set},
      list (Pervasives.result unit e) → Pervasives.result unit (list e).

    Parameter all : ∀ {a e : Set},
      list (Pervasives.result a e) → Pervasives.result (list a) (list e).

    Parameter both : ∀ {a b e : Set},
      Pervasives.result a e → Pervasives.result b e →
      Pervasives.result (a × b) (list e).

    Parameter tzfail : ∀ {_error a : Set},
      _error → Pervasives.result a (trace _error).

    Parameter op_andstar : ∀ {a b e : Set},
      Pervasives.result a (trace e) → Pervasives.result b (trace e) →
      Pervasives.result (a × b) (trace e).

    Parameter op_andplus : ∀ {a b e : Set},
      Pervasives.result a (trace e) → Pervasives.result b (trace e) →
      Pervasives.result (a × b) (trace e).

    Parameter tzjoin : ∀ {_error : Set},
      list (Pervasives.result unit (trace _error)) →
      Pervasives.result unit (trace _error).

    Parameter tzall : ∀ {_error a : Set},
      list (Pervasives.result a (trace _error)) →
      Pervasives.result (list a) (trace _error).

    Parameter tzboth : ∀ {_error a b : Set},
      Pervasives.result a (trace _error) →
      Pervasives.result b (trace _error) →
      Pervasives.result (a × b) (trace _error).
  End Result_syntax.

  Module Lwt_result_syntax.
    Parameter _return : ∀ {a e : Set}, a → Pervasives.result a e.

    Parameter return_unit : ∀ {e : Set}, Pervasives.result unit e.

    Parameter return_none : ∀ {a e : Set}, Pervasives.result (option a) e.

    Parameter return_some : ∀ {a e : Set},
      a → Pervasives.result (option a) e.

    Parameter return_nil : ∀ {a e : Set}, Pervasives.result (list a) e.

    Parameter return_true : ∀ {e : Set}, Pervasives.result bool e.

    Parameter return_false : ∀ {e : Set}, Pervasives.result bool e.

    Parameter fail : ∀ {a e : Set}, e → Pervasives.result a e.

    Parameter op_letstar : ∀ {a b e : Set},
      Pervasives.result a e → (a → Pervasives.result b e) →
      Pervasives.result b e.

    Parameter op_letplus : ∀ {a b e : Set},
      Pervasives.result a e → (a → b) → Pervasives.result b e.

    Parameter lwt_map_error : ∀ {a e f : Set},
      (e → f) → Pervasives.result a e → Pervasives.result a f.

    Parameter op_letstarexclamation : ∀ {a b : Set}, a → (a → b) → b.

    Parameter op_letstarquestion : ∀ {a b e : Set},
      Pervasives.result a e → (a → Pervasives.result b e) →
      Pervasives.result b e.

    Parameter join : ∀ {e : Set},
      list (Pervasives.result unit e) → Pervasives.result unit (list e).

    Parameter all : ∀ {a e : Set},
      list (Pervasives.result a e) → Pervasives.result (list a) (list e).

    Parameter both : ∀ {a b e : Set},
      Pervasives.result a e → Pervasives.result b e →
      Pervasives.result (a × b) (list e).

    Parameter tzfail : ∀ {_error a : Set},
      _error → Pervasives.result a (trace _error).

    Parameter op_andstar : ∀ {a b e : Set},
      Pervasives.result a (trace e) → Pervasives.result b (trace e) →
      Pervasives.result (a × b) (trace e).

    Parameter op_andplus : ∀ {a b e : Set},
      Pervasives.result a (trace e) → Pervasives.result b (trace e) →
      Pervasives.result (a × b) (trace e).

    Parameter tzjoin : ∀ {_error : Set},
      list (Pervasives.result unit (trace _error)) →
      Pervasives.result unit (trace _error).

    Parameter tzall : ∀ {_error a : Set},
      list (Pervasives.result a (trace _error)) →
      Pervasives.result (list a) (trace _error).

    Parameter tzboth : ∀ {_error a b : Set},
      Pervasives.result a (trace _error) →
      Pervasives.result b (trace _error) →
      Pervasives.result (a × b) (trace _error).
  End Lwt_result_syntax.

  Module Lwt_option_syntax.
    Parameter _return : ∀ {a : Set}, a → option a.

    Parameter return_unit : option unit.

    Parameter return_nil : ∀ {a : Set}, option (list a).

    Parameter return_true : option bool.

    Parameter return_false : option bool.

    Parameter fail : ∀ {a : Set}, option a.

    Parameter op_letstar : ∀ {a b : Set},
      option a → (a → option b) → option b.

    Parameter op_andstar : ∀ {a b : Set},
      option a → option b → option (a × b).

    Parameter op_letplus : ∀ {a b : Set}, option a → (a → b) → option b.

    Parameter op_andplus : ∀ {a b : Set},
      option a → option b → option (a × b).

    Parameter op_letstarexclamation : ∀ {a b : Set}, a → (a → b) → b.

    Parameter op_letstarquestion : ∀ {a b : Set},
      option a → (a → option b) → option b.

    Parameter both : ∀ {a b : Set}, option a → option b → option (a × b).
  End Lwt_option_syntax.
End Error_monad_signature.
Require Export TezosOfOCaml.Environment.V8.Error_monad.
Module Error_monad_check : Error_monad_signature := Error_monad.

Export Error_monad.Notations.

Module Type Seq_signature.
  Reserved Notation "'t".

  Inductive node (a : Set) : Set :=
  | Nil : node a
  | Cons : a → 't a → node a
  
  where "'t" := (fun (t_a : Set) ⇒ unit → node t_a).

  Definition t := 't.

  Arguments Nil {_}.
  Arguments Cons {_}.

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

  Parameter _return : ∀ {a : Set}, a → t a.

  Parameter cons_value : ∀ {a : Set}, a → t a → t a.

  Parameter append : ∀ {a : Set}, t a → t a → t a.

  Parameter map : ∀ {a b : Set}, (a → b) → t a → t b.

  Parameter filter : ∀ {a : Set}, (a → bool) → t a → t a.

  Parameter filter_map : ∀ {a b : Set}, (a → option b) → t a → t b.

  Parameter flat_map : ∀ {a b : Set}, (a → t b) → t a → t b.

  Parameter fold_left : ∀ {a b : Set}, (a → b → a) → a → t b → a.

  Parameter iter : ∀ {a : Set}, (a → unit) → t a → unit.

  Parameter unfold : ∀ {a b : Set}, (b → option (a × b)) → b → t a.

  Parameter first : ∀ {a : Set}, t a → option a.

  Parameter fold_left_e : ∀ {a b trace : Set},
    (a → b → Pervasives.result a trace) → a → t b →
    Pervasives.result a trace.

  Parameter fold_left_s : ∀ {a b : Set}, (a → b → a) → a → t b → a.

  Parameter fold_left_es : ∀ {a b trace : Set},
    (a → b → Pervasives.result a trace) → a → t b →
    Pervasives.result a trace.

  Parameter iter_e : ∀ {a trace : Set},
    (a → Pervasives.result unit trace) → t a → Pervasives.result unit trace.

  Parameter iter_s : ∀ {a : Set}, (a → unit) → t a → unit.

  Parameter iter_es : ∀ {a trace : Set},
    (a → Pervasives.result unit trace) → t a → Pervasives.result unit trace.

  Parameter iter_ep : ∀ {a : Set}, (a → M? unit) → t a → M? unit.

  Parameter iter_p : ∀ {a : Set}, (a → unit) → t a → unit.
End Seq_signature.
Require Export TezosOfOCaml.Environment.V8.Seq.
Module Seq_check : Seq_signature := Seq.

Module Type List_signature.
  Definition t (a : Set) : Set := list a.

  Parameter nil : ∀ {a : Set}, list a.

  Parameter nil_e : ∀ {a trace : Set}, Pervasives.result (list a) trace.

  Parameter nil_s : ∀ {a : Set}, list a.

  Parameter nil_es : ∀ {a trace : Set}, Pervasives.result (list a) trace.

  Parameter cons_value : ∀ {a : Set}, a → list a → list a.

  Parameter is_empty : ∀ {a : Set}, list a → bool.

  Parameter hd : ∀ {a : Set}, list a → option a.

  Parameter tl : ∀ {a : Set}, list a → option (list a).

  Parameter nth : ∀ {a : Set}, list a → int → option a.

  Parameter nth_opt : ∀ {a : Set}, list a → int → option a.

  Parameter last : ∀ {a : Set}, a → list a → a.

  Parameter last_opt : ∀ {a : Set}, list a → option a.

  Parameter find : ∀ {a : Set}, (a → bool) → list a → option a.

  Parameter find_opt : ∀ {a : Set}, (a → bool) → list a → option a.

  Parameter find_map : ∀ {a b : Set},
    (a → option b) → list a → option b.

  Parameter mem : ∀ {a : Set}, (a → a → bool) → a → list a → bool.

  Parameter assoc : ∀ {a b : Set},
    (a → a → bool) → a → list (a × b) → option b.

  Parameter assoc_opt : ∀ {a b : Set},
    (a → a → bool) → a → list (a × b) → option b.

  Parameter assq : ∀ {a b : Set}, a → list (a × b) → option b.

  Parameter assq_opt : ∀ {a b : Set}, a → list (a × b) → option b.

  Parameter mem_assoc : ∀ {a b : Set},
    (a → a → bool) → a → list (a × b) → bool.

  Parameter mem_assq : ∀ {a b : Set}, a → list (a × b) → bool.

  Parameter remove_assoc : ∀ {a b : Set},
    (a → a → bool) → a → list (a × b) → list (a × b).

  Parameter remove_assq : ∀ {a b : Set}, a → list (a × b) → list (a × b).

  Parameter init_value : ∀ {a trace : Set},
    trace → int → (int → a) → Pervasives.result (list a) trace.

  Parameter length : ∀ {a : Set}, list a → int.

  Parameter rev : ∀ {a : Set}, list a → list a.

  Parameter concat : ∀ {a : Set}, list (list a) → list a.

  Parameter append : ∀ {a : Set}, list a → list a → list a.

  Parameter rev_append : ∀ {a : Set}, list a → list a → list a.

  Parameter flatten : ∀ {a : Set}, list (list a) → list a.

  Parameter combine : ∀ {a b trace : Set},
    trace → list a → list b → Pervasives.result (list (a × b)) trace.

  Parameter rev_combine : ∀ {a b trace : Set},
    trace → list a → list b → Pervasives.result (list (a × b)) trace.

  Parameter split : ∀ {a b : Set}, list (a × b) → list a × list b.

  Parameter iter2 : ∀ {a b trace : Set},
    trace → (a → b → unit) → list a → list b →
    Pervasives.result unit trace.

  Parameter map2 : ∀ {a b c trace : Set},
    trace → (a → b → c) → list a → list b →
    Pervasives.result (list c) trace.

  Parameter rev_map2 : ∀ {a b c trace : Set},
    trace → (a → b → c) → list a → list b →
    Pervasives.result (list c) trace.

  Parameter fold_left2 : ∀ {a b c trace : Set},
    trace → (a → b → c → a) → a → list b → list c →
    Pervasives.result a trace.

  Parameter fold_right2 : ∀ {a b c trace : Set},
    trace → (a → b → c → c) → list a → list b → c →
    Pervasives.result c trace.

  Parameter for_all2 : ∀ {a b trace : Set},
    trace → (a → b → bool) → list a → list b →
    Pervasives.result bool trace.

  Parameter _exists2 : ∀ {a b trace : Set},
    trace → (a → b → bool) → list a → list b →
    Pervasives.result bool trace.

  Parameter init_e : ∀ {a trace : Set},
    trace → int → (int → Pervasives.result a trace) →
    Pervasives.result (list a) trace.

  Parameter init_s : ∀ {a trace : Set},
    trace → int → (int → a) → Pervasives.result (list a) trace.

  Parameter init_es : ∀ {a trace : Set},
    trace → int → (int → Pervasives.result a trace) →
    Pervasives.result (list a) trace.

  Parameter init_p : ∀ {a trace : Set},
    trace → int → (int → a) → Pervasives.result (list a) trace.

  Parameter find_e : ∀ {a trace : Set},
    (a → Pervasives.result bool trace) → list a →
    Pervasives.result (option a) trace.

  Parameter find_s : ∀ {a : Set}, (a → bool) → list a → option a.

  Parameter find_es : ∀ {a trace : Set},
    (a → Pervasives.result bool trace) → list a →
    Pervasives.result (option a) trace.

  Parameter find_map_e : ∀ {a b trace : Set},
    (a → Pervasives.result (option b) trace) → list a →
    Pervasives.result (option b) trace.

  Parameter find_map_s : ∀ {a b : Set},
    (a → option b) → list a → option b.

  Parameter find_map_es : ∀ {a b trace : Set},
    (a → Pervasives.result (option b) trace) → list a →
    Pervasives.result (option b) trace.

  Parameter filter : ∀ {a : Set}, (a → bool) → list a → list a.

  Parameter filteri : ∀ {a : Set}, (int → a → bool) → list a → list a.

  Parameter find_all : ∀ {a : Set}, (a → bool) → list a → list a.

  Parameter rev_filter : ∀ {a : Set}, (a → bool) → list a → list a.

  Parameter rev_filteri : ∀ {a : Set},
    (int → a → bool) → list a → list a.

  Parameter rev_filter_some : ∀ {a : Set}, list (option a) → list a.

  Parameter filter_some : ∀ {a : Set}, list (option a) → list a.

  Parameter rev_filter_ok : ∀ {a b : Set},
    list (Pervasives.result a b) → list a.

  Parameter filter_ok : ∀ {a b : Set},
    list (Pervasives.result a b) → list a.

  Parameter rev_filter_error : ∀ {a b : Set},
    list (Pervasives.result a b) → list b.

  Parameter filter_error : ∀ {a b : Set},
    list (Pervasives.result a b) → list b.

  Parameter rev_filter_left : ∀ {a b : Set}, list (Either.t a b) → list a.

  Parameter filter_left : ∀ {a b : Set}, list (Either.t a b) → list a.

  Parameter rev_filter_right : ∀ {a b : Set},
    list (Either.t a b) → list b.

  Parameter filter_right : ∀ {a b : Set}, list (Either.t a b) → list b.

  Parameter rev_filter_e : ∀ {a trace : Set},
    (a → Pervasives.result bool trace) → list a →
    Pervasives.result (list a) trace.

  Parameter filter_e : ∀ {a trace : Set},
    (a → Pervasives.result bool trace) → list a →
    Pervasives.result (list a) trace.

  Parameter rev_filter_s : ∀ {a : Set}, (a → bool) → list a → list a.

  Parameter filter_s : ∀ {a : Set}, (a → bool) → list a → list a.

  Parameter rev_filter_es : ∀ {a trace : Set},
    (a → Pervasives.result bool trace) → list a →
    Pervasives.result (list a) trace.

  Parameter filter_es : ∀ {a trace : Set},
    (a → Pervasives.result bool trace) → list a →
    Pervasives.result (list a) trace.

  Parameter rev_filteri_e : ∀ {a trace : Set},
    (int → a → Pervasives.result bool trace) → list a →
    Pervasives.result (list a) trace.

  Parameter filteri_e : ∀ {a trace : Set},
    (int → a → Pervasives.result bool trace) → list a →
    Pervasives.result (list a) trace.

  Parameter rev_filteri_s : ∀ {a : Set},
    (int → a → bool) → list a → list a.

  Parameter filteri_s : ∀ {a : Set},
    (int → a → bool) → list a → list a.

  Parameter rev_filteri_es : ∀ {a trace : Set},
    (int → a → Pervasives.result bool trace) → list a →
    Pervasives.result (list a) trace.

  Parameter filteri_es : ∀ {a trace : Set},
    (int → a → Pervasives.result bool trace) → list a →
    Pervasives.result (list a) trace.

  Parameter rev_partition : ∀ {a : Set},
    (a → bool) → list a → list a × list a.

  Parameter partition : ∀ {a : Set},
    (a → bool) → list a → list a × list a.

  Parameter