Skip to main content

๐Ÿƒย Environment_modules.v

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import Proto_alpha.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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.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.
End Bytes_signature.
Require Export Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.Z.
Module Z_check : Z_signature := Z.

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.
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.

  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 bool_value : encoding bool.

  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 array_value : โˆ€ {a : Set},
    option int โ†’ encoding a โ†’ encoding (array a).

  Parameter list_value : โˆ€ {a : Set},
    option int โ†’ 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).

  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.

  Parameter string_enum : โˆ€ {a : Set}, list (string ร— a) โ†’ encoding a.

  Module Fixed.
    Parameter string_value : int โ†’ encoding string.

    Parameter bytes_value : int โ†’ encoding bytes.

    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 bytes_value : encoding bytes.

    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_value : int โ†’ encoding string.

    Parameter bytes_value : int โ†’ encoding bytes.
  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 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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.TzEndian.
Module TzEndian_check : TzEndian_signature := TzEndian.

Module Type Bits_signature.
  Parameter numbits : int โ†’ int.
End Bits_signature.
Require Export Proto_alpha.Environment.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 Proto_alpha.Environment.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 Proto_alpha.Environment.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 fail : โˆ€ {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 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).
  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).
  End Lwt_result_syntax.

  Module Tzresult_syntax.
    Parameter _return : โˆ€ {_error a : Set},
      a โ†’ Pervasives.result a _error.

    Parameter return_unit : โˆ€ {_error : Set},
      Pervasives.result unit _error.

    Parameter return_none : โˆ€ {_error a : Set},
      Pervasives.result (option a) _error.

    Parameter return_some : โˆ€ {_error a : Set},
      a โ†’ Pervasives.result (option a) _error.

    Parameter return_nil : โˆ€ {_error a : Set},
      Pervasives.result (list a) _error.

    Parameter return_true : โˆ€ {_error : Set},
      Pervasives.result bool _error.

    Parameter return_false : โˆ€ {_error : Set},
      Pervasives.result bool _error.

    Parameter fail : โˆ€ {_error a : Set},
      _error โ†’ Pervasives.result a (trace _error).

    Parameter op_letstar : โˆ€ {a b e : Set},
      Pervasives.result a e โ†’ (a โ†’ Pervasives.result b e) โ†’
      Pervasives.result b e.

    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_letplus : โˆ€ {a b e : Set},
      Pervasives.result a e โ†’ (a โ†’ b) โ†’ Pervasives.result b 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 join : โˆ€ {_error : Set},
      list (Pervasives.result unit (trace _error)) โ†’
      Pervasives.result unit (trace _error).

    Parameter all : โˆ€ {_error a : Set},
      list (Pervasives.result a (trace _error)) โ†’
      Pervasives.result (list a) (trace _error).

    Parameter both : โˆ€ {_error a b : Set},
      Pervasives.result a (trace _error) โ†’
      Pervasives.result b (trace _error) โ†’
      Pervasives.result (a ร— b) (trace _error).
  End Tzresult_syntax.

  Module Lwt_tzresult_syntax.
    Parameter _return : โˆ€ {_error a : Set},
      a โ†’ Pervasives.result a _error.

    Parameter return_unit : โˆ€ {_error : Set},
      Pervasives.result unit _error.

    Parameter return_none : โˆ€ {_error a : Set},
      Pervasives.result (option a) _error.

    Parameter return_some : โˆ€ {_error a : Set},
      a โ†’ Pervasives.result (option a) _error.

    Parameter return_nil : โˆ€ {_error a : Set},
      Pervasives.result (list a) _error.

    Parameter return_true : โˆ€ {_error : Set},
      Pervasives.result bool _error.

    Parameter return_false : โˆ€ {_error : Set},
      Pervasives.result bool _error.

    Parameter fail : โˆ€ {_error a : Set},
      _error โ†’ Pervasives.result a (trace _error).

    Parameter op_letstar : โˆ€ {a b e : Set},
      Pervasives.result a e โ†’ (a โ†’ Pervasives.result b e) โ†’
      Pervasives.result b e.

    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_letplus : โˆ€ {a b e : Set},
      Pervasives.result a e โ†’ (a โ†’ b) โ†’ Pervasives.result b 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 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 : โˆ€ {_error : Set},
      list (Pervasives.result unit (trace _error)) โ†’
      Pervasives.result unit (trace _error).

    Parameter all : โˆ€ {_error a : Set},
      list (Pervasives.result a (trace _error)) โ†’
      Pervasives.result (list a) (trace _error).

    Parameter both : โˆ€ {_error a b : Set},
      Pervasives.result a (trace _error) โ†’
      Pervasives.result b (trace _error) โ†’
      Pervasives.result (a ร— b) (trace _error).
  End Lwt_tzresult_syntax.
End Error_monad_signature.
Require Export Proto_alpha.Environment.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 Proto_alpha.Environment.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 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 rev_partition_map : โˆ€ {a b c : Set},
    (a โ†’ Either.t b c) โ†’ list a โ†’ list b ร— list c.

  Parameter partition_map : โˆ€ {a b c : Set},
    (a โ†’ Either.t b c) โ†’ list a โ†’ list b ร— list c.

  Parameter rev_partition_result : โˆ€ {a b : Set},
    list (Pervasives.result a b) โ†’ list a ร— list b.

  Parameter partition_result : โˆ€ {a b : Set},
    list (Pervasives.result a b) โ†’ list a ร— list b.

  Parameter rev_partition_either : โˆ€ {a b : Set},
    list (Either.t a b) โ†’ list a ร— list b.

  Parameter partition_either : โˆ€ {a b : Set},
    list (Either.t a b) โ†’ list a ร— list b.

  Parameter rev_partition_e : โˆ€ {a trace : Set},
    (a โ†’ Pervasives.result bool trace) โ†’ list a โ†’
    Pervasives.result (list a ร— list a) trace.

  Parameter partition_e : โˆ€ {a trace : Set},
    (a โ†’ Pervasives.result bool trace) โ†’ list a โ†’
    Pervasives.result (list a ร— list a) trace.

  Parameter rev_partition_s : โˆ€ {a : Set},
    (a โ†’ bool) โ†’ list a โ†’ list a ร— list a.

  Parameter partition_s : โˆ€ {a : Set},
    (a โ†’ bool) โ†’ list a โ†’ list a ร— list a.

  Parameter rev_partition_es : โˆ€ {a trace : Set},
    (a โ†’ Pervasives.result bool trace) โ†’ list a โ†’
    Pervasives.result (list a ร— list a) trace.

  Parameter partition_es : โˆ€ {a trace : Set},
    (a โ†’ Pervasives.result bool trace) โ†’ list a โ†’
    Pervasives.result (list a ร— list a) trace.

  Parameter partition_p : โˆ€ {a : Set},
    (a โ†’ bool) โ†’ list a โ†’ list a ร— list a.

  Parameter rev_partition_map_e : โˆ€ {a b c trace : Set},
    (a โ†’ Pervasives.result (Either.t b c) trace) โ†’ list a โ†’
    Pervasives.result (list b ร— list c) trace.

  Parameter partition_map_e : โˆ€ {a b c trace : Set},
    (a โ†’ Pervasives.result (Either.t b c) trace) โ†’ list a โ†’
    Pervasives.result (list b ร— list c) trace.

  Parameter rev_partition_map_s : โˆ€ {a b c : Set},
    (a โ†’ Either.t b c) โ†’ list a โ†’ list b ร— list c.

  Parameter partition_map_s : โˆ€ {a b c : Set},
    (a โ†’ Either.t b c) โ†’ list a โ†’ list b ร— list c.

  Parameter rev_partition_map_es : โˆ€ {a b c trace : Set},
    (a โ†’ Pervasives.result (Either.t b c) trace) โ†’ list a โ†’
    Pervasives.result (list b ร— list c) trace.

  Parameter partition_map_es : โˆ€ {a b c trace : Set},
    (a โ†’ Pervasives.result (Either.t b c) trace) โ†’ list a โ†’
    Pervasives.result (list b ร— list c) trace.

  Parameter iter : โˆ€ {a : Set}, (a โ†’ unit) โ†’ list a โ†’ unit.

  Parameter iter_e : โˆ€ {a trace : Set},
    (a โ†’ Pervasives.result unit trace) โ†’ list a โ†’
    Pervasives.result unit trace.

  Parameter iter_s : โˆ€ {a : Set}, (a โ†’ unit) โ†’ list a โ†’ unit.

  Parameter iter_es : โˆ€ {a trace : Set},
    (a โ†’ Pervasives.result unit trace) โ†’ list a โ†’
    Pervasives.result unit trace.

  Parameter iter_p : โˆ€ {a : Set}, (a โ†’ unit) โ†’ list a โ†’ unit.

  Parameter iteri : โˆ€ {a : Set}, (int โ†’ a โ†’ unit) โ†’ list a โ†’ unit.

  Parameter iteri_e : โˆ€ {a trace : Set},
    (int โ†’ a โ†’ Pervasives.result unit trace) โ†’ list a โ†’
    Pervasives.result unit trace.

  Parameter iteri_s : โˆ€ {a : Set}, (int โ†’ a โ†’ unit) โ†’ list a โ†’ unit.

  Parameter iteri_es : โˆ€ {a trace : Set},
    (int โ†’ a โ†’ Pervasives.result unit trace) โ†’ list a โ†’
    Pervasives.result unit trace.

  Parameter iteri_p : โˆ€ {a : Set}, (int โ†’ a โ†’ unit) โ†’ list a โ†’ unit.

  Parameter map : โˆ€ {a b : Set}, (a โ†’ b) โ†’ list a โ†’ list b.

  Parameter map_e : โˆ€ {a b trace : Set},
    (a โ†’ Pervasives.result b trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter map_s : โˆ€ {a b : Set}, (a โ†’ b) โ†’ list a โ†’ list b.

  Parameter map_es : โˆ€ {a b trace : Set},
    (a โ†’ Pervasives.result b trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter map_p : โˆ€ {a b : Set}, (a โ†’ b) โ†’ list a โ†’ list b.

  Parameter mapi : โˆ€ {a b : Set}, (int โ†’ a โ†’ b) โ†’ list a โ†’ list b.

  Parameter mapi_e : โˆ€ {a b trace : Set},
    (int โ†’ a โ†’ Pervasives.result b trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter mapi_s : โˆ€ {a b : Set}, (int โ†’ a โ†’ b) โ†’ list a โ†’ list b.

  Parameter mapi_es : โˆ€ {a b trace : Set},
    (int โ†’ a โ†’ Pervasives.result b trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter mapi_p : โˆ€ {a b : Set}, (int โ†’ a โ†’ b) โ†’ list a โ†’ list b.

  Parameter rev_map : โˆ€ {a b : Set}, (a โ†’ b) โ†’ list a โ†’ list b.

  Parameter rev_mapi : โˆ€ {a b : Set}, (int โ†’ a โ†’ b) โ†’ list a โ†’ list b.

  Parameter rev_map_e : โˆ€ {a b trace : Set},
    (a โ†’ Pervasives.result b trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter rev_map_s : โˆ€ {a b : Set}, (a โ†’ b) โ†’ list a โ†’ list b.

  Parameter rev_map_es : โˆ€ {a b trace : Set},
    (a โ†’ Pervasives.result b trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter rev_map_p : โˆ€ {a b : Set}, (a โ†’ b) โ†’ list a โ†’ list b.

  Parameter rev_mapi_e : โˆ€ {a b trace : Set},
    (int โ†’ a โ†’ Pervasives.result b trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter rev_mapi_s : โˆ€ {a b : Set},
    (int โ†’ a โ†’ b) โ†’ list a โ†’ list b.

  Parameter rev_mapi_es : โˆ€ {a b trace : Set},
    (int โ†’ a โ†’ Pervasives.result b trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter rev_mapi_p : โˆ€ {a b : Set},
    (int โ†’ a โ†’ b) โ†’ list a โ†’ list b.

  Parameter rev_filter_map : โˆ€ {a b : Set},
    (a โ†’ option b) โ†’ list a โ†’ list b.

  Parameter rev_filter_map_e : โˆ€ {a b trace : Set},
    (a โ†’ Pervasives.result (option b) trace) โ†’ list a โ†’
    Pervasives.result (list b) trace.

  Parameter filter_map_e : โˆ€ {a b trace : Set},
    (